Commit 2022-11-25 11:49 2c459900

View on Github →

chore(algebra/big_operators/multiset): split (#17712) Split algebra.big_operators.multiset into .basic and .lemmas, with the former containing no algebra imports. This should make more of the fintype dependency tree portable sooner. A follow-up on #17702 (for list). See the latest graph for the motivation.

Estimated changes

Modified src/algebra/big_operators/basic.lean

Renamed src/algebra/big_operators/multiset.lean to src/algebra/big_operators/multiset/basic.lean

deleted theorem commute.multiset_sum_left

deleted theorem commute.multiset_sum_right

deleted theorem multiset.dvd_prod

deleted theorem multiset.prod_eq_one_iff

Created src/algebra/big_operators/multiset/lemmas.lean

added theorem commute.multiset_sum_left

added theorem commute.multiset_sum_right

added theorem multiset.dvd_prod

added theorem multiset.prod_eq_one_iff

Modified src/algebra/hom/freiman.lean

Modified src/data/list/prime.lean

Modified src/data/multiset/bind.lean