OAI/RepresentationTheory/FoulkesHowe/FiniteDimension.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.Problem346.finiteDimensional_symPow line 12

   Source documentation

   Every homogeneous symmetric power of a finite-dimensional complex space is finite dimensional. The proof uses its tensor-power presentation.

   instance finiteDimensional_symPow (n : ℕ) (V : Type u) [AddCommGroup V]
       [Module ℂ V] [FiniteDimensional ℂ V] : FiniteDimensional ℂ (SymPow n V) :=
   …

   Mentions: OAI.Problem346.SymPow