mathlib

774e6803 - feat(data/fintype/basic): add noncomputable equivalences between finsets as fintypes and `fin s.card`, etc. (#15080)

feat(data/fintype/basic): add noncomputable equivalences between finsets as fintypes and `fin s.card`, etc. (#15080) As `s.card` is not defeq to `fintype.card s`, it is convenient to have these definitions in addition to `fintype.equiv_fin` and others (though we omit the computable ones). Co-authored-by: Wrenna Robson <34025592+linesthatinterlace@users.noreply.github.com>