leanprover-community/mathlib

Pull Requests Commits

Merge branch 'master' into SP_factorization_add_sub

stuart-presnell committed 3 years ago

8637c368

feat(analysis/seminorm): Add construction of seminorm over normed fields (#15893)

mcdoll committed 3 years ago

d032ed1d

feat(topology): composition of continuous functions is continuous w.r.t. the compact-open topologies (#15721)

faenuccio committed 3 years ago

7e20c8fc

chore(set_theory/cardinal/ordinal): follow your linter (#16265)

adomani committed 3 years ago

1b8a0c29

chore(order/bounded_order): Rename `is_complemented` to `complemented_lattice` (#16263)

YaelDillies committed 3 years ago

daec7d61

feat(order/heyting/regular): Heyting-regular elements (#16033)

YaelDillies committed 3 years ago

24b08ce6

feat(algebra/char_p/basic + data/zmod/basic): the characteristic is the order of one and zmod related lemmas (#16277)

adomani committed 3 years ago

e4b9af26

feat(data/nat/factorization/basic): lemmas about `n.factorization p = 0` (#16185)

stuart-presnell committed 3 years ago

8ad70779

Add lemma `factorization_sub_iff`

stuart-presnell committed 3 years ago

9f1a0c9c

feat(linear_algebra/affine_space/affine_subspace): `map_eq_bot_iff` (#16285)

jsm28 committed 3 years ago

211bf1ab

feat(linear_algebra/affine_space/affine_equiv): lemmas about coercion to `affine_map` (#16284)

jsm28 committed 3 years ago

39d5a98c

feat(data/rat/cast): generalize `ext` lemmas (#16268)

urkud committed 3 years ago

3e2fb4c7

refactor(algebra/order/with_zero): Generalize lemmas (#16240)

YaelDillies committed 3 years ago

31297bda

feat(ring_theory/polynomial/basic): generalize `is_domain` to `no_zero_divisors` (#16226)

eric-wieser committed 3 years ago

301a6253

feat(counterexamples/map_floor): `floor`/`ceil` are not preserved under order ring homs (#16198)

YaelDillies committed 3 years ago

9c0a5431

feat(topology/algebra/polynomial): add coeff_le_of_roots_le (#15275)

xroblot committed 3 years ago

ae93ce85

feat(category_theory/preadditive): projective iff variants of Yoneda preserve epimorphisms (#15123)

TwoFX committed 3 years ago

f0514a8f

feat(algebra/order/positive): new file (#14833)

urkud committed 3 years ago

24a233d4

feat(measure_theory/function/conditional_expectation/basic): add some condexp lemmas (#16273)

kex-y committed 3 years ago

7c4a46f3

feat(data/rat/nnrat): Nonnegative rationals (#16283)

YaelDillies committed 3 years ago

6de241f9

stuart-presnell committed 3 years ago

018f0e6a

stuart-presnell committed 3 years ago

6312c024

Prove `factorization_add_iff`

stuart-presnell committed 3 years ago

ddc2d35f

feat(probability/integration): remove integrability assumption in indep_fun.integral_mul (#16167)

sgouezel committed 3 years ago

de62604b

chore(category_theory): fix name of mono_app_of_mono (#16275)

joelriou committed 3 years ago

937c692d

fix(combinatorics/composition): remove non-terminal simp (#16259)

gebner committed 3 years ago

8dd80093

feat(algebra/order/field): Canonically linear ordered semifields (#15677)

YaelDillies committed 3 years ago

1c2d71f1

feat(data/rat/defs): add two lemmas for `pnat_denom` of 0 and 1 (#15864)

joneugster committed 3 years ago

ebb53dc3

chore(category_theory/limits/shapes/finite_products): avoid tidy (#16261)

gebner committed 3 years ago

6901db60

docs(ring_theory/valuation/valuation_subring): clarify value group docstring (#16272)

kbuzzard committed 3 years ago

c241a033

Older