mathlib
ec9476fd - chore(data/fintype/basic): add card_le_of_surjective and card_quotient_le (#6964)

Commit
4 years ago
chore(data/fintype/basic): add card_le_of_surjective and card_quotient_le (#6964) Add two natural lemmas that were missing from `fintype.basic`. Co-authored-by: Adrián Doña Mateo <43966663+AdrianDoM@users.noreply.github.com>
Author
Parents
Loading