Integral normalization in coefficient coordinates

The lower coefficients of the integral normalization of a nonzero degree n polynomial f are f.coeff i * f.leadingCoeff ^ (n - 1 - i). Expressing the normalization through monicOfCoeff makes sense even when these coefficients specialize to a lower-degree polynomial: the monic leading term is retained. This is the coefficient construction needed to normalize analytic families across a vanishing leading coefficient.

Polynomial.isRoot_integralNormalization_mul_iff recovers the original root equation from a normalized root scaled by the leading coefficient, including zero and constant polynomials.

theorem TauCeti.Polynomial.monicOfCoeff_mul_pow_eq_integralNormalization {R : Type u_1} [CommSemiring R] [Nontrivial R] {f : Polynomial R} {n : ℕ} (hf : f ≠ 0) (hdeg : f.natDegree = n) : (monicOfCoeff fun (i : Fin n) => f.coeff ↑i * f.leadingCoeff ^ (n - 1 - ↑i)) = f.integralNormalization

Integral normalization is the monic polynomial with its explicitly scaled lower coefficients. Keeping the degree parameter fixed in this expression permits specialization through a degree drop.

theorem Polynomial.isRoot_integralNormalization_mul_iff {K : Type u_1} [CommSemiring K] [IsDomain K] (f : Polynomial K) (z : K) : f.integralNormalization.IsRoot (f.leadingCoeff * z) ↔ f.IsRoot z

Integral normalization preserves the root equation after scaling by the leading coefficient. This includes the zero polynomial and nonzero constants.