Commit 2024-12-09 11:16 888b1efe

View on Github →

refactor: unbundle Multiset.card (#19777) This is a first step towards not importing algebra to define multisets.

Estimated changes

Modified Mathlib/Algebra/BigOperators/Finsupp.lean

added theorem Multiset.card_finsuppSum

Modified Mathlib/Algebra/BigOperators/Group/Finset.lean

added theorem Multiset.card_sum

Modified Mathlib/Combinatorics/Additive/FreimanHom.lean

Modified Mathlib/Combinatorics/Optimization/ValuedCSP.lean

modified def FractionalOperation.size

Modified Mathlib/Data/Multiset/Basic.lean

modified def Multiset.card

added def Multiset.cardHom

modified theorem Multiset.card_add

modified theorem Multiset.card_nsmul

Modified Mathlib/Data/Sym/Basic.lean

Modified Mathlib/RingTheory/UniqueFactorizationDomain/NormalizedFactors.lean