leanprover-community/mathlib3

Pull Requests Commits

Update noetherian.lean

alreadydone committed 3 years ago

Verified c07f8f61

Merge branch 'master' into eric-wieser/submodule.map2

eric-wieser committed 3 years ago

Verified 24eb19c5

eric-wieser committed 3 years ago

91d6c5a3

one more lemma, remove underscore

eric-wieser committed 3 years ago

6053c184

chore(ring_theory/*): dot notation for `submodule.fg` and `subalgebra.fg` (#13737)

eric-wieser committed 3 years ago

ccd37746

doc(order/filter/small_sets): fix in doc (#13648)

fpvandoorn committed 3 years ago

220d4b89

feat(set_theory/game/birthday): Game birthday is zero iff empty (#13715)

vihdzp committed 3 years ago

c096a33a

feat(cyclotomic/eval): (q - 1) ^ totient n < |ϕₙ(q)| (#12595)

ericrbg committed 3 years ago

8a32fdfd

feat(ring_theory/submonoid/membership): generalize a few lemmas to `mul_mem_class` (#13748)

j-loreaux committed 3 years ago

0d3f8a71

fix(group_theory/subsemigroup/basic): change `mul_one_class` to `has_mul` (#13747)

j-loreaux committed 3 years ago

c5bf4808

chore(*/equiv): missing refl_symm lemmas (#13761)

kim-em committed 3 years ago

1c92dfdf

feat(set_theory/ordinal/basic): `max a 0 = a` (#13734)

vihdzp committed 3 years ago

0cb20fca

feat(set_theory/game/pgame): Right moves of nat game are empty (#13730)

vihdzp committed 3 years ago

98e78488

feat(set_theory/game/pgame): An empty game is a relabelling of `0` (#13753)

vihdzp committed 3 years ago

a0af1474

fix(ring_theory/subsemiring/basic): make `inclusion` a `ring_hom`, not a `monoid_hom` (#13746)

j-loreaux committed 3 years ago

e89510c2

feat(logic/unit): Make `punit.star` simp normal form of `default : punit` (#13741)

vihdzp committed 3 years ago

60bb0711

fix(topology/bornology): turn `bounded_space` into a `mixin` (#13615)

urkud committed 3 years ago

dc589c89

feat(measure_theory/measure/finite_measure_weak_convergence): define the topology of weak convergence of measures and prove some lemmas about it. (#9943)

kkytola committed 3 years ago

d3997443

perf(representation_theory/basic): speed up `representation.lin_hom` by a factor of 20 (#13739)

eric-wieser committed 3 years ago

ccefda07

eric-wieser committed 3 years ago

597d7dca

add set.image2_eq_Union

eric-wieser committed 3 years ago

4c48dfbf

feat(combinatorics/simple_graph/regularity/uniform): Witnesses of non-uniformity (#13155)

YaelDillies committed 3 years ago

5ac5c922

feat(representation_theory/basic): representation theory without scalar actions (#13573)

antoinelab01 committed 3 years ago

cb2b02ff

feat(set_theory/game/pgame): Define `is_option` relation (#13700)

vihdzp committed 3 years ago

79e309b7

fix(data/set/basic): fix name of `has_mem.mem.out` (#13721)

fpvandoorn committed 3 years ago

48997d7b

eric-wieser committed 3 years ago

7d432885

refactor(number_theory/padics/padic_norm): split file (#13576)

BoltonBailey committed 3 years ago

b00a7f8a

eric-wieser committed 3 years ago

643609d0

eric-wieser committed 3 years ago

cecb8c0a

chore(topology/continuous_function/zero_at_infty): add `is_central_scalar` instance (#13710)

eric-wieser committed 3 years ago

de79a763

Older