Commit 2025-02-20 13:00 49411456

View on Github →

chore(Data/Finset): don't import algebra when defining Finset.card (#21866) This PR aims to define Finset.card and Fintype.card without importing anything from the algebra library. In addition to the changes of #21840, we modify a few proofs and move a few lemmas so that Data.Finset.Card doesn't need to know about monoids.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Combinatorics/SetFamily/Intersecting.lean

Modified Mathlib/Combinatorics/SimpleGraph/Triangle/Removal.lean

Modified Mathlib/Data/Finset/Card.lean

deleted theorem Finset.cast_card_erase_of_mem

deleted theorem Finset.cast_card_inter

deleted theorem Finset.cast_card_sdiff

deleted theorem Finset.cast_card_union

Created Mathlib/Data/Finset/CastCard.lean

added theorem Finset.cast_card_erase_of_mem

added theorem Finset.cast_card_inter

added theorem Finset.cast_card_sdiff

added theorem Finset.cast_card_union

Modified Mathlib/Data/Finset/Grade.lean

Modified Mathlib/Data/Finset/NatAntidiagonal.lean

Modified Mathlib/Data/Finset/Sum.lean

Modified Mathlib/Data/Fintype/Card.lean

Modified Mathlib/Data/Fintype/Pi.lean

Modified Mathlib/RingTheory/MvPolynomial/Symmetric/NewtonIdentities.lean