Discharge of the cycle-type transport hypotheses

cycleType_permCongr and cycleType_sigmaCongrRight discharge the PermCongrCT and SigmaCT hypotheses: the colour cycle sum and the Frobenius formula for the Jacobi–Trudi character hold unconditionally.

theorem RS.permCongrCT : PermCongrCT

Transport preserves cycle type, discharging the colour cycle sum's hypothesis.

theorem RS.sigmaCT : SigmaCT

And so does the fibrewise congruence, discharging the Frobenius formula's.

theorem RS.jtChar_frobenius' (μ : YoungDiagram) (t : ℕ → ℂ) : (↑μ.card.factorial)⁻¹ * ∑ π : Equiv.Perm (Fin μ.card), jtChar μ π * cycleProd t π = diagramSchur μ t

The Frobenius formula for the Jacobi–Trudi character, unconditionally: its normalized cycle-weighted sum is the Jacobi–Trudi determinant.