Commits leanprover-community/mathlib3

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

feat(algebra/homology): some elementwise lemmas (#12997)

kim-em committed 3 years ago

eba31b58

feat(algebra/*): coe_to_equiv_symm simp lemmas (#12996)

kim-em committed 3 years ago

dacf0490

feat(measure_theory/functions/strongly_measurable): almost everywhere strongly measurable functions (#12985)

sgouezel committed 3 years ago

f0c15be6

chore(data/polynomial/ring_division): remove nontrivial assumptions (#12984)

eric-wieser committed 3 years ago

fd2c6c47

feat({ring_theory,group_theory}/localization): add some small lemmas for localisation API (#12861)

jjaassoonn committed 3 years ago

c0421e76

feat(ring_theory/localization): lemmas about `Frac(R)`-spans (#12425)

Vierkantor committed 3 years ago

1ebb2060

doc(data/polynomial/field_division): fix broken docstring links (#12981)

eric-wieser committed 3 years ago

e48f2e82

doc({linear_algebra,matrix}/charpoly): add crosslinks (#12980)

eric-wieser committed 3 years ago

d31410ab

feat(topology/continuous_on): add `set.maps_to.closure_of_continuous_on` (#12975)

urkud committed 3 years ago

597cbf10

feat(data/list/big_operators): add multiplicative versions (#12966)

urkud committed 3 years ago

ff72aa22

feat(data/polynomial/ring_division): `mem_root_set_iff` (#12963)

vihdzp committed 3 years ago

443c239d

chore(data/matrix/basic): square matrices over a non-unital ring form a non-unital ring (#12913)

eric-wieser committed 3 years ago

162d83fc

feat(set_theory/cardinal): `cardinal.to_nat` is order-preserving on finite cardinals (#12763)

tb65536 committed 3 years ago

c030dd2a

feat(set_theory/cofinality): Lemmas relating `cof` to `lsub` and `blsub` (#12316)

vihdzp committed 3 years ago

2873b7ac

feat(topology/continuous/algebra) : giving `C(α, M)` a `has_continuous_mul` and a `has_continuous_smul` structure (#11261)

laughinggas committed 3 years ago

b7d6b3aa

feat(order/hom/*): equivalences mapping morphisms to their dual (#12888)

YaelDillies committed 3 years ago

77110125

chore(test/matrix): clean up an unused argument (#12986)

alexjbest committed 3 years ago

587af996

feat(measure_theory/measure): add some simp lemmas, golf (#12974)

urkud committed 3 years ago

562bbf52

feat(data/list/pairwise): `pairwise_of_forall_mem_list` (#12968)

vihdzp committed 3 years ago

4b05a42d

chore(analysis/analytic/basic): golf (#12965)

urkud committed 3 years ago

73a9c27f