FoulkesMultilinear.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem346.monomialMultilinearAux line 12
theorem OAI.Problem346.monomialMultilinearAux_apply line 19
def OAI.Problem346.foulkesIndexEquiv line 25
Source documentation
Reindex the slots in a transposed grid, allowing an independent permutation in each original row.
```
def foulkesIndexEquiv (a b : ℕ) (σ : Fin b → Equiv.Perm (Fin a)) :
    (Σ _ : Fin a, Fin b) ≃ (Fin b × Fin a) where
…
```

def OAI.Problem346.foulkesSummandMultilinear line 34

Source documentation

A summand of the Foulkes--Howe formula, viewed as a multilinear map in all entries of the input grid.

def foulkesSummandMultilinear (a b : ℕ) (V : Type u)
    [AddCommGroup V] [Module ℂ V] (σ : Fin b → Equiv.Perm (Fin a)) :
    MultilinearMap ℂ (fun _ : Fin b × Fin a => V) (SymPow a (SymPow b V)) :=
…

Mentions: OAI.Problem346.SymPow

theorem OAI.Problem346.foulkesSummandMultilinear_apply line 40
def OAI.Problem346.foulkesMultilinear line 49
Source documentation
The canonical Foulkes--Howe expression is multilinear in its a * b individual vector arguments.
```
def foulkesMultilinear (a b : ℕ) (V : Type u)
    [AddCommGroup V] [Module ℂ V] :
    MultilinearMap ℂ (fun _ : Fin b × Fin a => V) (SymPow a (SymPow b V)) := by
…
```
Mentions: OAI.Problem346.SymPow
theorem OAI.Problem346.foulkesMultilinear_apply line 56