Canonical multiplicative factors of a power of ω, at every exponent

The canonical multiplicatively principal factors of ω ^ α are ω raised to the Cantor terms of α, so the residual factor deletes the least such term. SuccessorFactorization is the case of positive constant Cantor coefficient, where deleting the least term is deleting 1.

theorem Ordinal.multiplicativePrincipalFactors_omega0_opow (alpha : Ordinal.{u}) : (omega0 ^ alpha).multiplicativePrincipalFactors = List.map (fun (a : Ordinal.{u}) => omega0 ^ a) alpha.additivePrincipalTerms

theorem Ordinal.residualFactor_omega0_opow (alpha : Ordinal.{u}) (hadd : (omega0 ^ alpha).IsAdditivelyPrincipal) (hone : 1 < omega0 ^ alpha) : AdditivePrincipalAboveOne.residualFactor ⟨omega0 ^ alpha, ⋯⟩ = omega0 ^ alpha.additivePrincipalTerms.dropLast.sum

theorem Ordinal.principalFactor_omega0_opow (alpha : Ordinal.{u}) (hadd : (omega0 ^ alpha).IsAdditivelyPrincipal) (hone : 1 < omega0 ^ alpha) (hne : alpha.additivePrincipalTerms ≠ []) : AdditivePrincipalAboveOne.principalFactor ⟨omega0 ^ alpha, ⋯⟩ = omega0 ^ alpha.additivePrincipalTerms.getLast hne