leanprover-community/mathlib3

Pull Requests Commits

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

refactor(topology/{separation,subset_properties}): use `set.subsingleton` (#12232)

urkud committed 3 years ago

3e77124c

feat(analysis/normed_space/linear_isometry): add lemmas to `linear_isometry_equiv` (#12218)

Daniel-Packer committed 3 years ago

dc9b8bea

feat(ring_theory/ideal/over): `S/p` is noetherian over `R/p` if `S` is over `R` (#12183)

Vierkantor committed 3 years ago

f44ed74a

fix(algebra/star/basic): more type classes that should be props (#12235)

dupuisf committed 3 years ago

515eefaf

feat(group_theory/perm): add lemmas for cycles of permutations (#11955)

AntoineChambert-Loir committed 3 years ago

98bcabb0

feat(number_theory/cyclotomic/discriminant): discriminant of a p-th cyclotomic field (#11804)

riccardobrasca committed 3 years ago

0eed60e3

feat(algebra/algebra/spectrum): add spectral mapping for inverses (#12219)

j-loreaux committed 3 years ago

257bddff

fix(analysis/normed_space/star/basic): make prop type classes props (#12233)

dupuisf committed 3 years ago

e77675d2

feat(model_theory/basic): Language operations (#12129)

awainverse committed 3 years ago

264dd7ff

doc(number_theory/padics/*): typo in references (#12229)

kbuzzard committed 3 years ago

7cc4eb9d

chore(analysis): rename times_cont_diff (#12227)

PatrickMassot committed 3 years ago

42388681

refactor(combinatorics/simple_graph/{basic,degree_sum}): move darts from degree_sum to basic (#12195)

kmill committed 3 years ago

541a1a02

feat(ring_theory/localization): add a fintype instance (#12150)

ericrbg committed 3 years ago

f6ec999f

feat(algebra/module,linear_algebra): some `restrict_scalars` lemmas (#12181)

Vierkantor committed 3 years ago

e89222a6

feat(algebra/group/{hom,prod}): has_mul and mul_hom.prod (#12110)

pechersky committed 3 years ago

2ab3e2fa

feat(topology/algebra/group): add subgroup lemmas (#12026)

mariainesdff committed 3 years ago

18d1bdfc

feat(topology/algebra/group): add continuity lemmas (#11975)

mariainesdff committed 3 years ago

b60b7904

feat(set_theory/ordinal): `Inf_empty` (#12226)

vihdzp committed 3 years ago

64c8d217

docs(set_theory/ordinal): Remove mention of `omin` from docs (#12224)

vihdzp committed 3 years ago

d990681c

feat(set_theory/ordinal_arithmetic): `out_nonempty_iff_ne_zero` (#12223)

vihdzp committed 3 years ago

f7b6f421

chore(analysis/specific_limits): simplify proof of `cauchy_series_of_le_geometric` (#12215)

ecstatic-morse committed 3 years ago

e50ebde5

chore(linear_algebra/basic): golf `linear_equiv.smul_of_unit` (#12190)

eric-wieser committed 3 years ago

48ddfd55

refactor(model_theory/terms_and_formulas): Improvements to basics of first-order formulas (#12091)

awainverse committed 3 years ago

6bb8f229

Newer Older