Commit 2025-01-07 09:21 7d091da8

View on Github →

chore: don't import algebra in Data.Finset.Basic (#19779)

Estimated changes

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

added theorem Multiset.toFinset_card_eq_one_iff

added theorem Multiset.toFinset_eq_singleton_iff

added theorem Multiset.toFinset_nsmul

Modified Mathlib/Algebra/Order/Group/Multiset.lean

added theorem Multiset.Nodup.le_nsmul_iff_le

added theorem Multiset.dedup_nsmul

Modified Mathlib/Algebra/Polynomial/FieldDivision.lean

Modified Mathlib/Data/Finset/Basic.lean

deleted theorem Multiset.toFinset_eq_singleton_iff

deleted theorem Multiset.toFinset_nsmul

Modified Mathlib/Data/Finset/Card.lean

deleted theorem Multiset.toFinset_card_eq_one_iff

Modified Mathlib/Data/Finset/Defs.lean

Modified Mathlib/Data/Finset/Disjoint.lean

Modified Mathlib/Data/Finset/Lattice/Lemmas.lean

Modified Mathlib/Data/Finsupp/Multiset.lean

Modified Mathlib/Data/Multiset/Dedup.lean

deleted theorem Multiset.Nodup.le_nsmul_iff_le

deleted theorem Multiset.dedup_nsmul

Modified Mathlib/Data/Multiset/NatAntidiagonal.lean

Modified Mathlib/Data/Multiset/Nodup.lean

Modified Mathlib/Data/Multiset/Range.lean

Modified Mathlib/Data/Multiset/Sum.lean

Modified Mathlib/RingTheory/Radical.lean