Commit 2024-09-30 10:30 04f66c4a

View on Github →

chore: Finsupp.coe_finset_sum simp (#17228) From LeanCamCombi

Estimated changes

Modified Mathlib/Algebra/BigOperators/Finsupp.lean

modified theorem Finsupp.coe_finset_sum

modified theorem Finsupp.coe_sum

Modified Mathlib/Data/Nat/Factorization/Defs.lean