OAI/RepresentationTheory/FoulkesHowe/ProductVanishing.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem346.vanishing_on_products_aux line 14

   Source documentation

   Quadratic stabilization of diagonal vanishing on products. Both differential transfers and all of the induction hypotheses are discharged in this theorem.

   theorem vanishing_on_products_aux (V : Type u)
       [AddCommGroup V] [Module ℂ V] [FiniteDimensional ℂ V]
       (a b : ℕ) (ha : 1 ≤ a) (hb : 1 ≤ b) (hab : a*(a-1) ≤ b)
       (T : SymmetricMultilinearForm a b V)
       (hT : IsSymmetricMultilinearForm a b V T)
       (hdiag : ∀ y : Fin b → V, T (fun _ => symMonomial b V y) = 0) : T = 0 := by
   …

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