leanprover-community/mathlib

Pull Requests Commits

Merge branch 'master' into buchholz

vihdzp committed 3 years ago

d8f775cd

chore(data/nat/gcd): move nat.coprime.mul_add_mul_ne_mul (#13022)

Ruben-VandeVelde committed 3 years ago

ef7298d4

feat(algebra/algebra/unitization): add star structure for the unitization of a non-unital algebra (#13120)

j-loreaux committed 3 years ago

e1eb0bd9

feat(category_theory/monoidal): define monoidal structures on cartesian products of monoidal categories, (lax) monoidal functors and monoidal natural transformations (#13033)

manzyuk committed 3 years ago

e41208d8

feat(set_theory/cardinal_ordinal): Add `simp` lemmas for `aleph` (#13056)

vihdzp committed 3 years ago

bb5e5986

feat(measure_theory/measure/haar_lebesgue): measure of an affine subspace is zero (#13137)

urkud committed 3 years ago

d4b40c35

feat(order/filter/basic): add `filter.eventually_{eq,le}.prod_map` (#13103)

urkud committed 3 years ago

7617942c

feat(algebra/regular/basic): add lemma commute.is_regular_iff (#13104)

adomani committed 3 years ago

a29bd58d

vihdzp committed 3 years ago

3febff5c

vihdzp committed 3 years ago

f088bfd8

Merge branch 'aleph_simp_lemmas' into buchholz

vihdzp committed 3 years ago

d9794d21

chore(topology/vector_bundle): use continuous-linear rather than linear in core construction (#13053)

hrmacbeth committed 3 years ago

8e476fa4

vihdzp committed 3 years ago

69673b6a

refactor(topology/{fiber_bundle, vector_bundle}): make trivializations data rather than an existential (#13052)

hrmacbeth committed 3 years ago

cf6f27ee

feat(probability/independence): two lemmas on indep_fun (#13126)

vbeffara committed 3 years ago

3164b1ad

feat(group_theory/free_product): add (m)range_eq_supr (#12956)

nomeata committed 3 years ago

1d5b99b2

chore(algebra/order/ring): generalisation linter (#13096)

kim-em committed 3 years ago

7df59077

feat(model_theory/semantics): A simp lemma for `Theory.model` (#13117)

awainverse committed 3 years ago

607f4f8a

feat(topology/bornology/basic): alternate way of defining a bornology by its bounded set (#13064)

ADedecker committed 3 years ago

6dad5f8c

feat(topology/support): add lemma `locally_finite.exists_finset_nhd_mul_support_subset` (#13006)

ocfnash committed 3 years ago

6cf5dc53

feat(dynamics/periodic_pts): Lemma about periodic point from periodic point of iterate (#12940)

vihdzp committed 3 years ago

912f195f

vihdzp committed 3 years ago

a5b15098

feat(set_theory/ordinal_arithmetic): Coefficients of Cantor Normal Form (#12681)

vihdzp committed 3 years ago

196a48c8

feat(topology/[subset_properties, separation]): bornologies for filter.co[closed_]compact (#12927)

ADedecker committed 3 years ago

a3c753c4

docs(probability/martingale): missing word (#13113)

agjftucker committed 3 years ago

e8ef7449

feat(model_theory/syntax,semantics): Sentences for binary relation properties (#13087)

awainverse committed 3 years ago

b3653717

feat(data/polynomial/coeff): add `char_zero` instance on polynomials (#13075)

adomani committed 3 years ago

342a4b0a

feat(topology/algebra/uniform_group): add characterization of total boundedness (#12808)

mcdoll committed 3 years ago

89275df0

chore(model_theory/elementary_maps): Fix Tarski-Vaught Test (#13102)

awainverse committed 3 years ago

c61f7e88

chore(algebra/order/*): generalisation linter (#13098)

kim-em committed 3 years ago

e6a0a266

Older