leanprover-community/mathlib3

Pull Requests Commits

docstring, prefer le

hparshall committed 3 years ago

87c1c2bd

hparshall committed 3 years ago

0a29439a

feat(analysis/inner_product_space/sqrt): `is_self_adjoint.sqrt`

hparshall committed 3 years ago

467f7149

feat(topology,analysis): any function is continuous/differentiable on a subsingleton (#12293)

urkud committed 3 years ago

0f1bc2c0

refactor(topology,analysis): use `maps_to` in lemmas like `continuous_on.comp` (#12294)

urkud committed 3 years ago

bfc05842

feat(analysis/inner_product_space/spectrum): `has_eigenvalue_eigenvalues` (#12304)

hparshall committed 3 years ago

d2d6f178

feat(topology/compact_open): `simp`-lemmas for `compact_open.gen` (#12267)

tb65536 committed 3 years ago

d6a8e5d7

feat(category_theory/limits): more opposite-related transformations of cones (#12165)

TwoFX committed 3 years ago

7201c3b4

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

Older