Commit 2025-09-16 10:16 bad1fcc9

View on Github →

feat: grind annotations for Finset.card (#29429)

Estimated changes

Modified Archive/Imo/Imo1998Q2.lean

Modified Counterexamples/AharoniKorman.lean

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

Modified Mathlib/Combinatorics/Additive/PluenneckeRuzsa.lean

Modified Mathlib/Combinatorics/Hall/Finite.lean

Modified Mathlib/Combinatorics/SetFamily/Compression/UV.lean

Modified Mathlib/Combinatorics/SetFamily/HarrisKleitman.lean

Modified Mathlib/Combinatorics/SetFamily/KruskalKatona.lean

Modified Mathlib/Combinatorics/SetFamily/Shadow.lean

Modified Mathlib/Combinatorics/SimpleGraph/DeleteEdges.lean

Modified Mathlib/Combinatorics/SimpleGraph/Extremal/Turan.lean

Modified Mathlib/Combinatorics/SimpleGraph/Finite.lean

Modified Mathlib/Combinatorics/SimpleGraph/FiveWheelLike.lean

Modified Mathlib/Combinatorics/SimpleGraph/Operations.lean

Modified Mathlib/Combinatorics/SimpleGraph/Regularity/Chunk.lean

Modified Mathlib/Combinatorics/SimpleGraph/Regularity/Equitabilise.lean

Modified Mathlib/Combinatorics/SimpleGraph/StronglyRegular.lean

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

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

Modified Mathlib/Data/Finset/Card.lean

modified theorem Finset.card_insert_eq_ite

modified theorem Finset.card_insert_le

modified theorem Finset.card_inter

modified theorem Finset.card_le_card_sdiff_add_card

modified theorem Finset.card_pair_eq_one_or_two

modified theorem Finset.card_sdiff

modified theorem Finset.card_sdiff_add_card_eq_card

modified theorem Finset.card_sdiff_eq_card_sdiff_iff

modified theorem Finset.card_sdiff_le_card_sdiff_iff

modified theorem Finset.card_sdiff_lt_card_sdiff_iff

added theorem Finset.card_sdiff_of_subset

modified theorem Finset.card_singleton_inter

modified theorem Finset.card_union

modified theorem Finset.card_union_le

modified theorem Finset.pred_card_le_card_erase

Modified Mathlib/Data/Finset/CastCard.lean

Modified Mathlib/Data/Finset/Insert.lean

modified theorem Finset.insert_eq_self

Modified Mathlib/Data/Finset/Interval.lean

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

added theorem Finset.insert_inter

added theorem Finset.inter_insert

Modified Mathlib/Data/Fintype/Card.lean

Modified Mathlib/Data/Nat/Totient.lean

Modified Mathlib/Data/Set/Card/Arithmetic.lean

Modified Mathlib/Geometry/Euclidean/Circumcenter.lean

Modified Mathlib/LinearAlgebra/Lagrange.lean

Modified Mathlib/LinearAlgebra/Multilinear/Basic.lean

Modified Mathlib/NumberTheory/JacobiSum/Basic.lean

Modified Mathlib/Order/Interval/Finset/Box.lean