Vector α n
and Sym α n
are fintypes when α
is. #
Equations
- Vector.fintype = Fintype.ofEquiv (Fin n → α) (Equiv.symm (Equiv.vectorEquivFin α n))
Equations
- instFintypeSym' = Quotient.fintype (Vector.Perm.isSetoid α n)
Equations
- instFintypeSym = Fintype.ofEquiv (Sym.Sym' α n) (Equiv.symm Sym.symEquivSym')