Commit 2025-12-31 20:48 a56aa81b

View on Github →

feat: Have equality form for #t - #s in addition to the inequality (#33419)

Estimated changes

Modified Mathlib/Data/Finset/Card.lean

added theorem Finset.card_sub_card_eq

modified theorem Finset.le_card_sdiff