OAI/RepresentationTheory/FoulkesHowe/PowerSpan.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem346.span_purePowers_eq_top line 14

   Source documentation

   Pure powers span each symmetric power, including degree zero.

   theorem span_purePowers_eq_top (b : ℕ) (V : Type u)
       [AddCommGroup V] [Module ℂ V] :
       Submodule.span ℂ (Set.range (fun x : V => symMonomial b V (fun _ => x))) = ⊤ := by
   …

   Mentions: OAI.Problem346.symMonomial

2. theorem OAI.Problem346.multilinear_eq_zero_of_pure_powers line 35

   Source documentation

   Multilinearity extends vanishing on independent pure powers to vanishing everywhere.

   theorem multilinear_eq_zero_of_pure_powers (a b : ℕ) (V : Type u)
       [AddCommGroup V] [Module ℂ V] {W : Type v} [AddCommGroup W] [Module ℂ W]
       (T : MultilinearMap ℂ (fun _ : Fin a => SymPow b V) W)
       (hT : ∀ x : Fin a → V, T (fun i => symMonomial b V (fun _ => x i)) = 0) :
       T = 0 := by
   …

   Mentions: OAI.Problem346.SymPow, OAI.Problem346.symMonomial

3. theorem OAI.Problem346.symmetricMultilinearForm_eq_zero_of_pure_powers line 46

   Source documentation

   Independent pure powers detect a symmetric multilinear form.

   theorem symmetricMultilinearForm_eq_zero_of_pure_powers (a b : ℕ) (V : Type u)
       [AddCommGroup V] [Module ℂ V]
       (T : SymmetricMultilinearForm a b V)
       (hT : ∀ x : Fin a → V, T (fun i => symMonomial b V (fun _ => x i)) = 0) :
       T = 0 :=
   …

   Mentions: OAI.Problem346.SymmetricMultilinearForm, OAI.Problem346.symMonomial