Commit 2024-02-11 21:58 80bf34f1

View on Github →

feat: (s ∩ t).card = s.card + t.card - (s ∪ t).card (#10224) once coerced to an AddGroupWithOne. Also unify Finset.card_disjoint_union and Finset.card_union_eq From LeanAPAP

Estimated changes

Modified Mathlib/Combinatorics/SetFamily/CauchyDavenport.lean

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

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

Modified Mathlib/Combinatorics/SetFamily/LYM.lean

Modified Mathlib/Combinatorics/SetFamily/Shatter.lean

Modified Mathlib/Combinatorics/SimpleGraph/Density.lean

Modified Mathlib/Combinatorics/SimpleGraph/Finite.lean

Modified Mathlib/Combinatorics/SimpleGraph/Operations.lean

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

Modified Mathlib/Data/Finset/Card.lean

deleted theorem Finset.card_disjoint_union

added theorem Finset.card_inter

added theorem Finset.card_union

deleted theorem Finset.card_union_eq

added theorem Finset.card_union_of_disjoint

added theorem Finset.cast_card_inter

added theorem Finset.cast_card_union

Modified Mathlib/Data/Finset/NAry.lean

Modified Mathlib/Data/Finset/Prod.lean

Modified Mathlib/Data/Nat/Count.lean

Modified Mathlib/Data/Nat/Multiplicity.lean

Modified Mathlib/FieldTheory/Finite/Basic.lean

Modified Mathlib/FieldTheory/PolynomialGaloisGroup.lean

Modified Mathlib/Geometry/Euclidean/Circumcenter.lean

Modified Mathlib/GroupTheory/Perm/Support.lean

Modified Mathlib/MeasureTheory/Measure/Haar/Basic.lean

Modified Mathlib/NumberTheory/LegendreSymbol/GaussEisensteinLemmas.lean

Modified Mathlib/NumberTheory/SmoothNumbers.lean

Modified Mathlib/RingTheory/Prime.lean