mathlib3

cad1a6c6 - feat(set_theory/cardinal/basic): lemmas about `#(finset α)` (#14850)

feat(set_theory/cardinal/basic): lemmas about `#(finset α)` (#14850) This PR does the following: - prove `mk_finset_of_fintype : #(finset α) = 2 ^ℕ fintype.card α` for `fintype α` - rename `mk_finset_eq_mk` to `mk_finset_of_infinite` to match the former - rename `mk_finset` to `mk_coe_finset` to avoid confusion with these two lemmas