Commit 2024-05-28 07:17 685be109

View on Github →

chore: Do not import MulAction in Data.Multiset.Bind (#13289) The import can easily be postponed by quite a bit.

Estimated changes

Modified Mathlib/Algebra/BigOperators/Basic.lean

modified theorem Finset.card_eq_sum_ones

Modified Mathlib/Algebra/BigOperators/Fin.lean

Modified Mathlib/Algebra/BigOperators/Pi.lean

Modified Mathlib/Algebra/Group/Nat.lean

Modified Mathlib/Data/Finset/Image.lean

Modified Mathlib/Data/Finset/Union.lean

Modified Mathlib/Data/Fintype/Basic.lean

Modified Mathlib/Data/Fintype/BigOperators.lean

Modified Mathlib/Data/Fintype/Card.lean

Modified Mathlib/Data/Fintype/CardEmbedding.lean

Modified Mathlib/Data/Fintype/Option.lean

Modified Mathlib/Data/Multiset/Bind.lean