leanprover-community/mathlib3

Pull Requests Commits

Proved `cof_cof`

vihdzp committed 3 years ago

7e882f18

vihdzp committed 3 years ago

e350d9eb

Merge branch 'master' into cofinality_refactor

vihdzp committed 3 years ago

984d5a76

feat(group_theory/torsion): define torsion groups (#11850)

Julian committed 3 years ago

05d8188c

feat(analysis/normed_space/finite_dimension): add a lemma about `inf_dist` (#12282)

urkud committed 3 years ago

3cc9ac40

chore(measure_theory/decomposition/lebesgue): tidy a proof (#12274)

eric-wieser committed 3 years ago

c127fc36

feat(topology/algebra/order/extr): extr on closure (#12281)

urkud committed 3 years ago

6653544f

feat(order/filter/extr): add `is_*_on.comp_maps_to` (#12280)

urkud committed 3 years ago

8c485a4c

feat(ring_theory/localization): random lemmata for edge cases (#12146)

ericrbg committed 3 years ago

c1443d66

feat(topology/spectral/hom): Spectral maps (#12228)

YaelDillies committed 3 years ago

dae1dfe9

feat(order/partition/equipartition): Equipartitions (#12023)

YaelDillies committed 3 years ago

f2fdef6f

feat(algebra/symmetrized): Define the symmetrization of a ring (#11399)

mans0954 committed 3 years ago

605ea9f3

chore(topology/continuous_function/bounded): add an is_central_scalar instance (#12272)

eric-wieser committed 3 years ago

f7518dbe

chore(*): update to 3.40.0c (#12212)

gebner committed 3 years ago

feb54736

feat(analysis/mean_inequalities): AM and GM are equal on a constant tuple (#12179)

Ruben-VandeVelde committed 3 years ago

d3d37017

feat(topology/algebra/group): homeomorphisms for div (#12251)

fpvandoorn committed 3 years ago

d620395d

feat(order/conditionally_complete_lattice.lean): two new lemmas (#12250)

fpvandoorn committed 3 years ago

ed9f73ca

test(instance_diamonds): verify that restrict_scalars produces no diamonds on the complex numbers (#12273)

eric-wieser committed 3 years ago

08406293

feat(algebra/punit_instances): mul_semiring_action (#12271)

ericrbg committed 3 years ago

a0d2c439

feat(topology/metric_space/lipschitz): add `set.maps_to` lemmas (#12266)

urkud committed 3 years ago

9dca6f42

chore(measure_theory/function/uniform_integrable): replace `ℕ` by a type verifying enough assumptions (#12242)

RemyDegenne committed 3 years ago

d011bf20

feat(probability/stopping): generalize `is_stopping_time.measurable_set_lt` and variants beyond `ℕ` (#12240)

RemyDegenne committed 3 years ago

34cfcd02

feat(measure_theory/group/prod): generalize topological groups to measurable groups (#11933)

fpvandoorn committed 3 years ago

79887c96

feat(topology/vector_bundle): `topological_vector_prebundle` (#8154)

Nicknamen committed 3 years ago

8429ec96

feat(data/equiv/option): option_congr (#12263)

eric-wieser committed 3 years ago

76b1e012

chore(geometry/euclidean): split repetitive proof (#12209)

Vierkantor committed 3 years ago

b8b1b578

feat(ring_theory/ideal,dedekind_domain): lemmas on `I ≤ I^e` and `I < I^e` (#12185)

Vierkantor committed 3 years ago

3d97cfb1

feat(measure_theory/function/ae_eq_fun): generalize scalar actions (#12248)

eric-wieser committed 3 years ago

9eb78a33

feat(measure_theory/integral/average): define `measure_theory.average` (#12128)

urkud committed 3 years ago

f6a7ad9e

chore(category_theory/adjunction/opposites): Forgotten `category_theory` namespace (#12256)

YaelDillies committed 3 years ago

f3ee4628

Older