Fintype { xs : List α // xs.length = n }

Stream: Is there code for X?

[Kim Morrison]

I was a bit surprised to find both of these missing:

import Mathlib

variable (n : Nat) (α : Type _)

example : { xs : List α // xs.length = n } ≃ (Fin n → α) := by exact? -- fails

variable  [Fintype α]

#synth Fintype { xs : List α // xs.length = n } -- fails

Does anyone have these on hand?

[Daniel Weber]

example : Fintype { xs : List α // xs.length = n } := inferInstanceAs (Fintype (Mathlib.Vector α n))

[Daniel Weber]

And docs#Equiv.vectorEquivFin

[Kim Morrison]

Thanks!