VanishingInduction.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem346.symmetric_form_curry_comp line 13

Source documentation

Fixing the first argument and pulling back all other arguments preserves symmetry.

theorem symmetric_form_curry_comp {r b m : ℕ}
    (T : SymmetricMultilinearForm (r+1) b V)
    (hT : IsSymmetricMultilinearForm (r+1) b V T)
    (z : SymPow b V) (L : SymPow m V →ₗ[ℂ] SymPow b V) :
    IsSymmetricMultilinearForm r m V ((T.curryLeft z).compLinearMap (fun _ => L)) := by
…

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

def OAI.Problem346.lowerProductForm line 30
Source documentation
The lower-arity form used in the stabilization induction.
```
def lowerProductForm (r m : ℕ)
    (T : SymmetricMultilinearForm (r+1) (r+m) V) (x t : V) :
    SymmetricMultilinearForm r m V :=
…
```
Mentions: OAI.Problem346.SymmetricMultilinearForm
theorem OAI.Problem346.lowerProductForm_apply line 36
theorem OAI.Problem346.lowerProductForm_symmetric line 43