Commits leanprover-community/mathlib3

chore(ring_theory/valuation/basic): be explicit with type coercions

eric-wieser committed 3 years ago

642af053

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

chore(topology/instances/rat): rename to rat_lemmas (#12246)

eric-wieser committed 3 years ago

e167efa1

feat(set_theory/ordinal_arithmetic): `is_normal.eq_iff_zero_and_succ` (#12222)

vihdzp committed 3 years ago

c5267895

feat(topology/order/hom): Continuous order homomorphisms (#12012)

YaelDillies committed 3 years ago

7de8137d

feat(measure_theory/measure): generalize scalar actions (#12187)

eric-wieser committed 3 years ago

b0fbd912

split(analysis/functional/gauge): Split off `analysis.seminorm` (#12054)

YaelDillies committed 3 years ago

d01b55f1

feat(ring_theory/unique_factorization_domain): add count_self (#12074)

mariainesdff committed 3 years ago

6179707b

feat(algebra/order/monoid_lemmas_gt_zero): introduce the type of positive elements and prove some lemmas (#11833)

adomani committed 3 years ago

6f1d90d3