Documentation

LeanPool.RegtsSevenster.RS.Classical.SchurTheory.JTSimple

The Jacobi–Trudi character is plus-or-minus a native character #

theorem RS.jtChar_pm_simple (μ : YoungDiagram) :
∃ (S₀ : Submodule (MonoidAlgebra ℂ (Equiv.Perm (Fin μ.card))) (MonoidAlgebra ℂ (Equiv.Perm (Fin μ.card)))), IsSimpleModule (MonoidAlgebra ℂ (Equiv.Perm (Fin μ.card))) ↥S₀ ∧ ((∀ (π : Equiv.Perm (Fin μ.card)), jtChar μ π = nChar S₀ π) ∨ ∀ (π : Equiv.Perm (Fin μ.card)), jtChar μ π = -nChar S₀ π)

The Jacobi–Trudi character is ± a single native character.