Commits leanprover-community/mathlib

chore: update scripts/port_status for more flexible tagging (#17056)

kim-em committed 3 years ago

0578d23f

chore(algebra/*): mark frozen files that have been ported to mathlib4 (#17039)

kim-em committed 3 years ago

97bdf517

chore(logic/basic): add move eq_true from core, as eq_true_iff (#17060)

kim-em committed 3 years ago

4aa2a2e1

feat(ring_theory/discrete_valuation_ring): add not_is_field (#16979)

mariainesdff committed 3 years ago

7cc9c7ad

feat(algebra/squarefree): squarefree gcds of squarefree elements (#16999)

alexjbest committed 3 years ago

ccbe476c

fix(topology/algebra/uniform_mul_action): remove duplicate typeclasses (#17063)

ocfnash committed 3 years ago

98e8d557

feat(ring_theory/hahn_series): Loosen definition of additive valuation (#17057)

khwilson committed 3 years ago

cb8faf79

feat(geometry/manifold/cont_mdiff): add various properties (#16980)

fpvandoorn committed 3 years ago

91b33017

feat(analysis/asymptotics): prove that a function has derivative 0 using asymptotics (#16934)

fpvandoorn committed 3 years ago

8bf24777

feat(number_theory/kummer_dedekind): define conductor and add basic API plus theorem (#16833)

Paul-Lez committed 3 years ago

813725f8

chore(probability/independence): simplify the definition of pi_Union_Inter (#17043)

RemyDegenne committed 3 years ago

0b045c73

refactor(data/finsupp/ne_locus): Match `dist` API (#17036)

YaelDillies committed 3 years ago

22e33e9d

feat(data/multiset/interval): locally finite order on multisets (#17028)

eric-wieser committed 3 years ago

056a7a1a

feat(algebraic_geometry/prime_spectrum/noetherian): The spectrum of a noetherian ring is noetherian. (#17016)

erdOne committed 3 years ago

689184f7

feat(topology/algebra/uniform_convergence): criterion for a vector subspace of `α → E` to be a TVS for the topology of 𝔖-convergence (#14857)

ADedecker committed 3 years ago

f01de4e1

chore(algebra/module/basic): reduce imports (#17042)

kim-em committed 3 years ago

edfb391a

chore(logic/equiv/basic): split into two files (#17038)

kim-em committed 3 years ago

9407b033

fix(data/set/basic): Fix `set.lt_iff_ssubset`. (#17047)

erdOne committed 3 years ago

8c9b0057

feat(order/upper_lower): Maps of upper sets (#17007)

YaelDillies committed 3 years ago

4af7699b

fix(topology/metric_space/gromov_hausdorff): squeeze all simps (#17049)

fpvandoorn committed 3 years ago

3d197c69

feat(measure_theory/measure): `measure_Union_null_iff` for Props (#17029)

alexjbest committed 3 years ago

0b480ff9

chore(order/lattice): add lemmas about `sup` and `inf` on `prod` (#17040)

eric-wieser committed 3 years ago

3812c1ce

feat(scripts/port_status): script to show currently portable files (#17009)

kim-em committed 3 years ago

6d4f6107

feat(*): add various order-related lemmas (#16918)

ocfnash committed 3 years ago

a5347cb9

feat(analysis/calculus/cont_diff): strengthen lemma (#16933)

fpvandoorn committed 3 years ago

38992f94

feat(combinatorics/simple_graph/regularity/bound): `positivity` extension (#16639)

YaelDillies committed 3 years ago

8f774b71

feat(data/polynomial): a couple of lemmas on nat degree and roots of maps (#16992)

alexjbest committed 3 years ago

d8dd620c

feat(ring_theory/finiteness): A morphism is finitely presented if the composition with a finite morphism is. (#15949)

erdOne committed 3 years ago

cf94743b

feat(topology/subset_properties, noetherian_space): Noetherian spaces have finite irreducible components. (#17015)

erdOne committed 3 years ago

6d94ff7b

refactor(geometry/manifold/cont_mdiff): split everything about mfderiv (#16982)

fpvandoorn committed 3 years ago

2b69cd5e