leanprover-community/mathlib3

Pull Requests Commits

dupuisf committed 3 years ago

8a57cfd8

fix lemma so it builds

dupuisf committed 3 years ago

16b210ea

Update src/data/fun_like/basic.lean

dupuisf committed 3 years ago

Verified 4c95dd9c

dupuisf committed 3 years ago

1bf588fb

did a bunch more

dupuisf committed 3 years ago

079c3574

embedding + algebra/group/hom

dupuisf committed 3 years ago

243ebd40

add fun_like stuff

dupuisf committed 3 years ago

fba265e7

doc(analysis/normed_space): fixed normed_star_monoid doc-string (#12296)

kim-em committed 3 years ago

43fb5162

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

Older