OAI/RepresentationTheory/FoulkesHowe/Polarization.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem346.span_diagonal_eq_span_range_of_detection line 13

   Source documentation

   A scalar-valued diagonal-detection principle upgrades to a spanning identity for the diagonal values of any symmetric multilinear map.

   theorem span_diagonal_eq_span_range_of_detection
       {V : Type u} {W : Type v} [AddCommGroup V] [Module ℂ V]
       [AddCommGroup W] [Module ℂ W] (n : ℕ)
       (detect : ∀ T : MultilinearMap ℂ (fun _ : Fin n => V) ℂ,
         (∀ (σ : Equiv.Perm (Fin n)) (x : Fin n → V), T (fun i => x (σ i)) = T x) →
         (∀ x : V, T (fun _ => x) = 0) → T = 0)
       (m : MultilinearMap ℂ (fun _ : Fin n => V) W)
       (hsym : ∀ (σ : Equiv.Perm (Fin n)) (x : Fin n → V),
         m (fun i => x (σ i)) = m x) :
       Submodule.span ℂ (Set.range (fun x : V => m (fun _ => x))) =
         Submodule.span ℂ (Set.range m) := by
   …