Polynomial.integralNormalization_coeff

theorem Polynomial.integralNormalization_coeff : ∀ {R : Type u} [inst : Semiring R] {f : Polynomial R} {i : ℕ}, f.integralNormalization.coeff i = if f.degree = ↑i then 1 else f.coeff i * f.leadingCoeff ^ (f.natDegree - 1 - i)

The theorem `Polynomial.integralNormalization_coeff` states that for any semiring `R`, any polynomial `f` over `R` and any natural number `i`, the coefficient of `X^i` in the integral normalization of `f` is 1 if the degree of `f` equals `i`. Otherwise, it is the product of the coefficient of `X^i` in `f` and the leading coefficient of `f` raised to the power of the natural degree of `f` minus `i` minus 1. Here, the leading coefficient of a polynomial is the coefficient of the highest power of `X` in it, and the natural degree of a polynomial enforces the degree of the polynomial to `ℕ`, by defining `natDegree 0 = 0`.

More concisely: For any semiring R, polynomial f over R, and natural number i, the coefficient of X^i in the integral normalization of f is the leading coefficient of f raised to the power of deg(f) - i, where deg(f) is the degree of f, if i equals deg(f). Otherwise, it is the coefficient of X^i in f.