Commits leanprover-community/mathlib3

feat(algebra/parity + data/{int, nat}/parity): parity lemmas for general semirings (#12718)

adomani committed 3 years ago

1f1289fc

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

leanprover-community-bot committed 3 years ago

cbd61731

chore(data/equiv/basic): use `option.elim` and `sum.elim` (#12724)

urkud committed 3 years ago

45061f36

chore(algebra/associated): move prime_dvd_prime_iff_eq (#12706)

Ruben-VandeVelde committed 3 years ago

b622d4df

feat(group_theory/submonoid/operations): monoids are isomorphic to themselves as submonoids (#12658)

Multramate committed 3 years ago

7ed4f2ce

feat(algebra/algebra/subalgebra/pointwise): lemmas about `*` and `to_submodule` (#12695)

eric-wieser committed 3 years ago

375419f9

feat(linear_algebra/matrix/determinant): special case of the matrix determinant lemma (#12682)

eric-wieser committed 3 years ago

7582e149

feat(algebra/big_operators/finprod): finite product of power is power of finite product (#12655)

Multramate committed 3 years ago

9c09965e

doc(algebra/hierarchy_design): fix my name (#12674)

eric-wieser committed 3 years ago

88a59785

feat(linear_algebra/matrix/nonsingular_inverse): Add `matrix.list_prod_inv_reverse` (#12691)

eric-wieser committed 3 years ago

530f0088

fix(set_theory/ordinal_arithmetic): remove redundant hypothesis from `CNF_rec` (#12680)

vihdzp committed 3 years ago

7a02c9e6

feat(linear_algebra/clifford_algebra/conjugation): add lemmas showing interaction between `involute` and `even_odd` (#12672)

eric-wieser committed 3 years ago

a3b39c6e

feat(group_theory/finiteness): quotient of fg is fg (#12652)

Multramate committed 3 years ago

48ffeb79

chore(category_theory/preadditive/projective_resolution): typo (#12702)

jjaassoonn committed 3 years ago

a98202b2

perf(analysis/convec/topology): remove topological_add_group.path_connected instance (#12675)

gebner committed 3 years ago

eefa4257

feat(model_theory/terms_and_formulas): Notation for terms and formulas from Flypitch (#12630)

awainverse committed 3 years ago

5b90340b

feat(ring_theory/graded_algebra/homogeneous_ideal): refactor `homogeneous_ideal` as a structure extending ideals (#12673)

jjaassoonn committed 3 years ago

d199eb99

feat(category_theory/monoidal): distribute tensor over direct sum (#12626)

kim-em committed 3 years ago

061d04b9

chore(category_theory/abelian/projective): fix typo (#12701)

jjaassoonn committed 3 years ago

078b213e

fix(category_theory/bicategory): remove spaces before closing parentheses (#12700)

yuma-mizuno committed 3 years ago

92e67597

chore(measure_theory): move and rename some lemmas (#12699)

urkud committed 3 years ago

0bd6dc2a

doc(data/equiv/encodable): +2 docstrings (#12698)

urkud committed 3 years ago

4b562f82

chore(cyclotomic/gal): update todo (#12693)

ericrbg committed 3 years ago

a3e0c85d

chore(algebra/module/basic): Move the scalar action earlier (#12690)

eric-wieser committed 3 years ago

77395f1e

feat(group_theory/abelianization): An application of the three subgroups lemma (#12677)

tb65536 committed 3 years ago

025fe7cb

chore(analysis/seminorm): Weaken typeclasses on `convex` and `locally_convex` lemmas (#12645)

mcdoll committed 3 years ago

b7978f39

feat(category_theory/preadditive) : definition of injective resolution (#12641)

jjaassoonn committed 3 years ago

53f6d687

refactor(linear_algebra/basic): split file (#12637)

kim-em committed 3 years ago

585d6419

feat(algebra/associated): add irreducible.not_dvd_one (#12686)

Ruben-VandeVelde committed 3 years ago

2ad9b39a

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

leanprover-community-bot committed 3 years ago

6d63c9be