Commit 2024-09-20 19:31 555be78e

View on Github →

feat(Data/Finset): card_eq_succ in terms of cons (#16951) Also add cons_ne_empty and make it simp, also to match insert_ne_empty

Estimated changes

added theorem Finset.cons_ne_empty