leanprover-community/mathlib

Pull Requests Commits

Merge remote-tracking branch 'origin/master' into eric-wieser/semi_normed_ring

eric-wieser committed 3 years ago

b629a3dc

feat(set_theory/cardinal/basic): cardinality of a powerset (#13786)

eric-wieser committed 3 years ago

58552fe0

feat(group_theory/subgroup/basic): `inclusion` lemmas (#13754)

YaelDillies committed 3 years ago

b2e0a2d0

feat(topology/instances/matrix): add `matrix` lemmas about `tsum` (#13677)

eric-wieser committed 3 years ago

8eb25641

chore(analysis/asymptotics/asymptotics): relax `normed_group` to `semi_normed_group` in lemmas (#13642)

eric-wieser committed 3 years ago

889e9564

feat(algebra/algebra/basic): add some lemmas about `subsemiring` and `algebra_map` (#13767)

astrainfinita committed 3 years ago

aab0b2df

feat(representation_theory/Rep): Rep k G is abelian (#13689)

kim-em committed 3 years ago

8abfb3ba

feat(data/list/basic): add `list.range_map` (#13777)

urkud committed 3 years ago

bc65b7cd

feat(topology/algebra/affine): a sufficiently small dilation of a point in the interior of a set lands in the interior (#13766)

ocfnash committed 3 years ago

992e26fa

chore(ring_theory/mv_polynomial/basic): golf (#13765)

astrainfinita committed 3 years ago

b4cad379

feat(set_theory/game/pgame): `x - 0 = x + 0` (#13731)

vihdzp committed 3 years ago

5c1ee352

chore(scripts): update nolints.txt (#13775)

leanprover-community-bot committed 3 years ago

7170b66c

chore(*/equiv): add simp to refl_apply and trans_apply where missing (#13760)

kim-em committed 3 years ago

ead85e61

feat(category_theory/monoidal): transport rigid structure over an equivalence (#13736)

kim-em committed 3 years ago

e294500e

feat(category_theory/braiding): pull back a braiding along a faithful functor (#13684)

kim-em committed 3 years ago

ccb9d64b

feat(representation_theory/Rep): the category of representations (#13683)

kim-em committed 3 years ago

8edb3d16

feat(ring_theory/localization/basic): generalize to semiring (#13459)

yuma-mizuno committed 3 years ago

11a4a745

chore(set_theory/surreal/basic): Allow dot notation on `pgame.numeric` (#13768)

YaelDillies committed 3 years ago

214e2f1c

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

Older