Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-06-04 03:56 be183e26

View on Github →

chore(data/finset|multiset|finsupp): reduce algebra/ imports (#7797)

Estimated changes

Modified src/algebra/big_operators/basic.lean

added theorem multiset.abs_sum_le_sum_abs

Modified src/algebra/big_operators/finsupp.lean

added theorem finsupp.mul_sum

added theorem finsupp.sum_mul

Modified src/algebra/gcd_monoid.lean

Modified src/algebra/group_power/lemmas.lean

deleted theorem list.prod_repeat

deleted theorem list.sum_repeat

deleted theorem nat.nsmul_eq_mul

Modified src/algebra/iterate_hom.lean

Modified src/algebra/monoid_algebra.lean

Modified src/data/finsupp/basic.lean

deleted theorem finsupp.mul_sum

deleted theorem finsupp.sum_mul

Modified src/data/finsupp/lattice.lean

Modified src/data/list/basic.lean

added theorem list.prod_repeat

added theorem list.sum_repeat

Modified src/data/list/indexes.lean

Modified src/data/list/perm.lean

Modified src/data/multiset/basic.lean

deleted theorem multiset.abs_sum_le_sum_abs

Modified src/data/multiset/range.lean

Modified src/data/mv_polynomial/variables.lean

Modified src/data/nat/basic.lean

added theorem nat.nsmul_eq_mul

Modified src/linear_algebra/linear_independent.lean

Modified src/linear_algebra/multilinear.lean