Commit 2023-09-13 21:26 100e68cb

View on Github →

feat: add Finset.card_le_one_iff_subsingleton and Finset.one_lt_card_iff_nontrivial (#7131) The versions for Fintype already exist but are missing for Finset.

Estimated changes

Modified Mathlib/Data/Finset/Card.lean

added theorem Finset.card_le_one_iff_subsingleton_coe

added theorem Finset.one_lt_card_iff_nontrivial_coe

Modified Mathlib/Data/Fintype/Card.lean