equiv from fin n coming from card = n

Stream: Is there code for X?

[Kevin Buzzard]

Do we have something like this? Asking for an UG.

import data.finset.card

example (S : Type) (v : finset S) (n : ℕ) (hv : v.card = n) : fin n ≃ v :=
sorry

[Adam Topaz]

docs#fintype.equiv_fin I think?

[Adam Topaz]

Plus some equiv for fins of the same size

[Adam Topaz]

Maybe docs#fin.congr ?

[Kevin Buzzard]

That should do it -- thanks!

[Adam Topaz]

That uses the wrong card, but there should be some equiv between fin m and fin n given m=n, I just don’t remember the name

[Adam Topaz]

oh it's docs#fin.cast

[Adam Topaz]

or docs#equiv.fin_congr