MonomialMultilinear.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem346.symMonomialMultilinear line 14
Source documentation
The product of degree-one generators, with its multilinearity bundled.
```
def symMonomialMultilinear (n : ℕ) (V : Type u)
    [AddCommGroup V] [Module ℂ V] :
    MultilinearMap ℂ (fun _ : Fin n => V) (SymPow n V) :=
…
```
Mentions: OAI.Problem346.SymPow
theorem OAI.Problem346.symMonomialMultilinear_apply line 22
theorem OAI.Problem346.symMonomial_permute line 26
def OAI.Problem346.monomialFunctional line 33
Source documentation
A functional on a symmetric power induces a symmetric multilinear form.
```
def monomialFunctional (a b : ℕ) (V : Type u)
    [AddCommGroup V] [Module ℂ V]
    (φ : SymPow a (SymPow b V) →ₗ[ℂ] ℂ) : SymmetricMultilinearForm a b V :=
…
```
Mentions: OAI.Problem346.SymPow, OAI.Problem346.SymmetricMultilinearForm
theorem OAI.Problem346.monomialFunctional_apply line 39
theorem OAI.Problem346.monomialFunctional_symmetric line 44

theorem OAI.Problem346.linearMap_eq_zero_of_symMonomial line 52

Source documentation

Monomial values determine every linear map out of a symmetric power.

theorem linearMap_eq_zero_of_symMonomial (n : ℕ) (V : Type u)
    [AddCommGroup V] [Module ℂ V] {W : Type v} [AddCommGroup W] [Module ℂ W]
    (φ : SymPow n V →ₗ[ℂ] W)
    (hφ : ∀ x : Fin n → V, φ (symMonomial n V x) = 0) : φ = 0 := by
…

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

theorem OAI.Problem346.monomialFunctional_eq_zero_iff line 71

def OAI.Problem346.plethysmFormMultilinear line 84

Source documentation

Flatten the a rows of b vector arguments of a form on SymPow b V.

def plethysmFormMultilinear (a b : ℕ) (V : Type u)
    [AddCommGroup V] [Module ℂ V] (T : SymmetricMultilinearForm a b V) :
    MultilinearMap ℂ (fun _ : Σ _ : Fin a, Fin b => V) ℂ :=
…

Mentions: OAI.Problem346.SymmetricMultilinearForm

theorem OAI.Problem346.plethysmFormMultilinear_apply line 90
theorem OAI.Problem346.plethysmFormMultilinear_inner_permute line 96
theorem OAI.Problem346.plethysmFormMultilinear_outer_permute line 105