BinaryVanishing.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem346.binary_diagonal_to_mixed_products line 16

Source documentation

The split-pencil consequence of diagonal vanishing, expressed using the graded multiplication and first-slot convention of the induction.

theorem binary_diagonal_to_mixed_products (r m : ℕ) (hr : 0 < r)
    (T : SymmetricMultilinearForm (r+1) (r+m) V)
    (hT : IsSymmetricMultilinearForm (r+1) (r+m) V T)
    (hdiag : ∀ y : Fin (r+m) → V, T (fun _ => symMonomial (r+m) V y) = 0)
    (x t : V) (y : Fin m → V) :
    T (Fin.cons
      (symPowMul r m (symMonomial r V (fun _ => t)) (symMonomial m V y))
      (fun _ : Fin r =>
        symPowMul r m (symMonomial r V (fun _ => x)) (symMonomial m V y))) = 0 := by
…

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