mathlib3
6a0412e9 - chore(data/fintype): generalise `to_finset_card` (#2316)

Commit
5 years ago
chore(data/fintype): generalise `to_finset_card` (#2316) Slight generalisation of a lemma, allowing a more flexible `fintype` instance. Also americanises some spelling. :-) Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au> Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Author
Parents
Loading