mathlib3
802f23cf - feat(data/fintype/basic): `set_fintype_card_eq_univ_iff` (#11244)

Commit
4 years ago
feat(data/fintype/basic): `set_fintype_card_eq_univ_iff` (#11244) Adds companion lemma to `set_fintype_card_le_univ`. This PR also moves several `set.to_finset` lemmas earlier in the file.
Author
Parents
Loading