Commit 2024-11-28 13:32 dc8397f7

View on Github →

feat: (t \ s).ncard = t.ncard - s.ncard in a ring (#19407) Version of Finset.cast_card_sdiff for Set.ncard. Also generalise ncard_diff. From Kneser (LeanCamCombi)

Estimated changes

Modified Mathlib/Data/Set/Card.lean

added theorem Set.cast_ncard_sdiff

modified theorem Set.ncard_diff