# mathlibdocumentation

data.polynomial.integral_normalization

# Theory of monic polynomials #

We define integral_normalization, which relate arbitrary polynomials to monic ones.

noncomputable def polynomial.integral_normalization {R : Type u} [semiring R] (f : polynomial R) :

If f : R[X] is a nonzero polynomial with root z, integral_normalization f is a monic polynomial with root leading_coeff f * z.

Moreover, integral_normalization 0 = 0.

Equations
@[simp]
theorem polynomial.integral_normalization_zero {R : Type u} [semiring R] :
theorem polynomial.integral_normalization_coeff {R : Type u} [semiring R] {f : polynomial R} {i : } :
= ite (f.degree = i) 1 (f.coeff i * f.leading_coeff ^ (f.nat_degree - 1 - i))
theorem polynomial.integral_normalization_coeff_degree {R : Type u} [semiring R] {f : polynomial R} {i : } (hi : f.degree = i) :
theorem polynomial.integral_normalization_coeff_nat_degree {R : Type u} [semiring R] {f : polynomial R} (hf : f 0) :
theorem polynomial.integral_normalization_coeff_ne_degree {R : Type u} [semiring R] {f : polynomial R} {i : } (hi : f.degree i) :
= f.coeff i * f.leading_coeff ^ (f.nat_degree - 1 - i)
theorem polynomial.monic_integral_normalization {R : Type u} [semiring R] {f : polynomial R} (hf : f 0) :
@[simp]
theorem polynomial.support_integral_normalization {R : Type u} [ring R] [is_domain R] {f : polynomial R} :
theorem polynomial.integral_normalization_eval₂_eq_zero {R : Type u} {S : Type v} [comm_ring R] [is_domain R] {p : polynomial R} (f : R →+* S) {z : S} (hz : p = 0) (inj : ∀ (x : R), f x = 0x = 0) :
theorem polynomial.integral_normalization_aeval_eq_zero {R : Type u} {S : Type v} [comm_ring R] [is_domain R] [ S] {f : polynomial R} {z : S} (hz : f = 0) (inj : ∀ (x : R), S) x = 0x = 0) :