The Schur package, unconditionally

Discharging the padding and branching inputs: the classical symmetric-group representation theory consumed by the development is a theorem of this tree.

noncomputable def RS.schurPackage : SchurPackage

The Schur package.

Equations

• RS.schurPackage = RS.schurPackageOf RS.three_pow_mul_factorial_ge RS.schurPackage._proof_1