Commit 2026-05-25 22:55 350e6d85
View on Github →feat(Data/Finset/Card): add card_{pair,triple}_eq_iff (#39840) Two simple lemmas which characterise when explicit finsets have maximal size.
feat(Data/Finset/Card): add card_{pair,triple}_eq_iff (#39840) Two simple lemmas which characterise when explicit finsets have maximal size.