Commit 2025-02-25 14:06 14be8da2

View on Github →

chore(Data/Set/Finite): avoid importing algebra in Data.Set.Finite (#21870) By moving a few lemmas we can avoid knowing about monoids when defining basic lemmas on finite sets.

Estimated changes

Modified Mathlib/Algebra/Group/TypeTags/Fintype.lean

Modified Mathlib/Data/DFinsupp/Defs.lean

Modified Mathlib/Data/Finsupp/Defs.lean

Modified Mathlib/Data/Fintype/EquivFin.lean

deleted theorem List.exists_pw_disjoint_with_card

Modified Mathlib/Data/Fintype/Perm.lean

Modified Mathlib/Data/List/ToFinsupp.lean

Modified Mathlib/Data/Set/Finite/Basic.lean

deleted theorem Directed.exists_mem_subset_of_finset_subset_biUnion

deleted def Set.fintypeBiUnion

Modified Mathlib/Data/Set/Finite/Lattice.lean

added theorem Directed.exists_mem_subset_of_finset_subset_biUnion

added def Set.fintypeBiUnion

Modified Mathlib/GroupTheory/GroupAction/CardCommute.lean

Modified Mathlib/GroupTheory/Perm/Cycle/PossibleTypes.lean

added theorem List.exists_pw_disjoint_with_card

Modified Mathlib/Logic/Denumerable.lean

Modified Mathlib/Logic/Equiv/List.lean

Modified MathlibTest/dfinsupp_notation.lean