leanprover-community/mathlib3

Pull Requests Commits

dupuisf committed 3 years ago

c750afc5

move back to separate file

dupuisf committed 3 years ago

01cdd3f8

move to weak_dual.lean

dupuisf committed 3 years ago

fd59c24d

seems to build now

dupuisf committed 3 years ago

7219325f

dupuisf committed 3 years ago

e2a2d5b9

dupuisf committed 3 years ago

61147e65

another perm bug

dupuisf committed 3 years ago

dbd46399

dupuisf committed 3 years ago

73b34826

100 char linter

dupuisf committed 3 years ago

5ed36140

gelfand space def

dupuisf committed 3 years ago

f2563ec2

fix build up to gelfand_space

dupuisf committed 3 years ago

c01ac2ba

subtype fun_like

dupuisf committed 3 years ago

4dde6ee0

dupuisf committed 3 years ago

944b0f76

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

Older