LinearCase.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem346.foulkesFormula_one line 11
def OAI.Problem346.foulkesOneEquiv line 19
Source documentation
The canonical Foulkes--Howe equivalence when the inner degree is one.
```
def foulkesOneEquiv (b : ℕ) (V : Type u) [AddCommGroup V] [Module ℂ V] :
    SymPow b (SymPow 1 V) ≃ₗ[ℂ] SymPow 1 (SymPow b V) :=
…
```
Mentions: OAI.Problem346.SymPow
theorem OAI.Problem346.foulkesOneEquiv_isFoulkesMap line 23

theorem OAI.Problem346.canonical_foulkes_howe_a_one_aux line 30

Source documentation

Degree-one stabilization, with no finite-dimensionality requirement.

theorem canonical_foulkes_howe_a_one_aux (V : Type u)
    [AddCommGroup V] [Module ℂ V] (b : ℕ) :
    ∃ μ : SymPow b (SymPow 1 V) →ₗ[ℂ] SymPow 1 (SymPow b V),
      IsFoulkesMap 1 b V μ ∧ Function.Bijective μ ∧
      ∀ ν : SymPow b (SymPow 1 V) →ₗ[ℂ] SymPow 1 (SymPow b V),
        IsFoulkesMap 1 b V ν → ν = μ := by
…

Mentions: OAI.Problem346.SymPow, OAI.Problem346.IsFoulkesMap