Commits leanprover-community/mathlib3

feat(data/polynomial/div): `a - b ∣ p.eval a - p.eval b` (#13021)

vihdzp committed 3 years ago

66509e13

chore(data/polynomial/eval): golf two proofs involving evals (#13020)

adomani committed 3 years ago

111d3a4a

feat(topology/algebra/group): add small topology lemma (#12931)

MantasBaksys committed 3 years ago

b87c2677

feat(topology/algebra/monoid): `finprod` is eventually equal to `finset.prod` (#13013)

urkud committed 3 years ago

89c8112f

feat(data/polynomial/derivative): if `p` is a polynomial, then `p.derivative.nat_degree ≤ p.nat_degree - 1` (#12948)

adomani committed 3 years ago

545c2655

feat(ring_theory/dedekind_domain/adic_valuation): add adic valuation on a Dedekind domain (#12712)

mariainesdff committed 3 years ago

4bf4d9df

feat(analysis/locally_convex): add balanced hull and core (#12537)

mcdoll committed 3 years ago

1ffd04c0

feat(data/list/chain): Simp lemma for `chain r a (l ++ b :: c :: m)` (#12969)

vihdzp committed 3 years ago

0f92307e

feat(order/hom/bounded): an order_iso maps top to top and bot to bot (#12862)

Paul-Lez committed 3 years ago

1cdbc356

feat(algebra/homology): three lemmas on homological complexes (#12742)

joelriou committed 3 years ago

b535c2d5

feat(category_theory/bicategory/coherence): prove the coherence theorem for bicategories (#12155)

yuma-mizuno committed 3 years ago

1084cee9

feat(set_theory/ordinal_arithmetic): Characterize principal multiplicative ordinals (#11701)

vihdzp committed 3 years ago

7b8b8f13

feat(measure_theory/constructions/borel_space): add `borelize` tactic (#12844)

urkud committed 3 years ago

ce3cecef

feat(set_theory/{ordinal_arithmetic, game/nim}): Minimum excluded ordinal (#12659)

vihdzp committed 3 years ago

5fb7b7b6

feat(number_theory/frobenius_number): Frobenius numbers (#9729)

cocohearts committed 3 years ago

5fcad214

feat(data/set/basic): Laws for n-ary image (#13011)

YaelDillies committed 3 years ago

7fea719c

chore(data/{nat,int,rat}/cast): add bundled version of `cast_id` lemmas (#13001)

eric-wieser committed 3 years ago

94800295

feat(algebra/field_power): add min_le_of_zpow_le_max (#12915)

mariainesdff committed 3 years ago

8c9dee1c

feat(group_theory/quotient_group): maps of quotients by powers of integers induced by group homomorphisms (#12811)

Multramate committed 3 years ago

223d9a19

feat(group_theory/complement): Transversals as functions (#12732)

tb65536 committed 3 years ago

1a2182cd

chore(analysis/*): move matrix definitions into their own file and generalize (#13007)

eric-wieser committed 3 years ago

40b142e0

feat(group_theory/group_action): add `commute.smul_{left,right}[_iff]` lemmas (#13003)

eric-wieser committed 3 years ago

ea97ca6b

feat(group_theory/group_action/opposite): Add `smul_eq_mul_unop` (#12995)

tb65536 committed 3 years ago

261a1953

refactor(algebra/group/to_additive + files containing even/odd): move many lemmas involving even/odd to the same file (#12882)

adomani committed 3 years ago

6fe0c3b1

refactor(measure_theory/group/fundamental_domain): allow `null_measurable_set`s (#12005)

urkud committed 3 years ago

958f6b02

chore(algebra/group_power/lemmas): turn `[zn]smul` lemmas into instances (#13002)

eric-wieser committed 3 years ago

abaabc8c

feat(category_theory): the category of small categories has all small limits (#12979)

kim-em committed 3 years ago

0e1387bb

feat(data/list/cycle): Define the empty cycle (#12967)

vihdzp committed 3 years ago

31e5ae22

feat(ring_theory/dedekind_domain/ideal): add lemmas about sup of ideal with irreducible (#12859)

Paul-Lez committed 3 years ago

0c6f0c2a

chore(algebra/homology/homotopy): cleanup (#12998)

kim-em committed 3 years ago

4ee988db