Commits leanprover-community/mathlib3

Generalize index types

ecstatic-morse committed 3 years ago

e155a5dd

Cauchy sequences remain Cauchy when composed with covariant operators

ecstatic-morse committed 3 years ago

f9f15000

Add `cauchy_seq_of_eventually_const`

ecstatic-morse committed 3 years ago

eb714269

Add `monotone.tendsto_at_top_at_top_or_eventually_eq` for ℕ and ℤ

ecstatic-morse committed 3 years ago

282cd56f

chore(algebra/covariant): pass the operator explicitly for `monotone.covariant`

ecstatic-morse committed 3 years ago

1179155f

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

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