Commit 2024-05-20 11:44 cad0ed8b

View on Github →

chore: Separate algebraic multiset lemmas (#12845) Resplit Algebra.BigOperators.Multiset.Basic and Algebra.BigOperators.Multiset.Lemmas into two new files:

Algebra.BigOperators.Group.Multiset for lemmas that require group-like structures (Monoid, Group, ...)
Algebra.BigOperators.Ring.Multiset for lemmas that require ring-like structures (MonoidWithZero, Ring, ...) Add assert_not_exists Ring in the former. Once #12974 lands, it will be strenghtenable to assert_not_exists MonoidWithZero.

Estimated changes

Modified Mathlib.lean

Renamed Mathlib/Algebra/BigOperators/Multiset/Basic.lean to Mathlib/Algebra/BigOperators/Group/Multiset.lean

added theorem Multiset.dvd_prod

added theorem Multiset.fst_prod

added theorem Multiset.snd_prod

deleted theorem Multiset.sum_map_mul_left

deleted theorem Multiset.sum_map_mul_right

modified theorem map_multiset_prod

Modified Mathlib/Algebra/BigOperators/Ring.lean

Renamed Mathlib/Algebra/BigOperators/Multiset/Lemmas.lean to Mathlib/Algebra/BigOperators/Ring/Multiset.lean

deleted theorem Multiset.dvd_prod

deleted theorem Multiset.fst_prod

added theorem Multiset.prod_map_add

modified theorem Multiset.prod_map_neg

added theorem Multiset.prod_map_sum

deleted theorem Multiset.snd_prod

added theorem Multiset.sum_map_mul_left

added theorem Multiset.sum_map_mul_right

Modified Mathlib/Algebra/Order/BigOperators/Group/Multiset.lean

Modified Mathlib/Algebra/Order/BigOperators/Ring/Multiset.lean

Modified Mathlib/Combinatorics/Additive/FreimanHom.lean

Modified Mathlib/Data/Finset/Card.lean

Modified Mathlib/Data/Multiset/Antidiagonal.lean

deleted theorem Multiset.prod_map_add

Modified Mathlib/Data/Multiset/Bind.lean

Modified Mathlib/Data/Multiset/Sections.lean

deleted theorem Multiset.prod_map_sum

Modified Mathlib/Data/PNat/Factors.lean