Commits leanprover-community/mathlib3

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

feat(topology/metric_space/basic): add a few lemmas (#12259)

urkud committed 3 years ago

ed555939

feat(algebra/module/basic): add `smul_right_inj` (#12252)

urkud committed 3 years ago

158550d5

feat(topology/metric_space): multiplicative opposites inherit the same `(pseudo_?)(e?)metric` and `uniform_space` (#12120)

eric-wieser committed 3 years ago

2939c77d

feat(analysis/normed_space/basic): use weaker assumptions (#12260)

urkud committed 3 years ago

890338d4

refactor(topology/instances): put `ℕ`, `ℤ`, and `ℚ` in separate files (#12207)

eric-wieser committed 3 years ago

620af85a

feat(algebra/associated): add decidable instances (#12230)

ericrbg committed 3 years ago

eae6ae37

feat(data/pfun): A new induction on pfun.fix (#12109)

BoltonBailey committed 3 years ago

2c74921e

feat(topology/algebra/continuous_monoid_hom): `to_continuous_map` is a `closed_embedding` (#12217)

tb65536 committed 3 years ago

9b333b26

feat(analysis/normed_space/star/spectrum): prove the spectral radius of a selfadjoint element in a C*-algebra is its norm. (#12211)

j-loreaux committed 3 years ago

f04ad9a1

chore(geometry/manifold/algebra/smooth_functions): golf module instance (#12247)

eric-wieser committed 3 years ago

b72cca41

docs(order/order_iso_nat): Added note on `exists_increasing_or_nonincreasing_subseq` (#12239)

vihdzp committed 3 years ago

3e2df830

feat(measure_theory/function/strongly_measurable): more basic properties of `strongly_measurable` (#12164)

RemyDegenne committed 3 years ago

162d060c

feat(ring_theory/localization): add mk' lemmas (#12081)

mariainesdff committed 3 years ago

3fe20d40

feat(ring_theory/graded_algebra): definitions and basic operations of homogeneous ideal (#10784)

jjaassoonn committed 3 years ago

0d5bed0e