# Documentation

Mathlib.RingTheory.Polynomial.IntegralNormalization

# Theory of monic polynomials #

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

noncomputable def Polynomial.integralNormalization {R : Type u} [] (f : ) :

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

Moreover, integralNormalization 0 = 0.

Instances For
theorem Polynomial.integralNormalization_coeff {R : Type u} [] {f : } {i : } :
= if then 1 else * ^ ( - i)
theorem Polynomial.integralNormalization_coeff_degree {R : Type u} [] {f : } {i : } (hi : ) :
theorem Polynomial.integralNormalization_coeff_natDegree {R : Type u} [] {f : } (hf : f 0) :
theorem Polynomial.integralNormalization_coeff_ne_degree {R : Type u} [] {f : } {i : } (hi : ) :
theorem Polynomial.integralNormalization_coeff_ne_natDegree {R : Type u} [] {f : } {i : } (hi : ) :
theorem Polynomial.monic_integralNormalization {R : Type u} [] {f : } (hf : f 0) :
@[simp]
theorem Polynomial.support_integralNormalization {R : Type u} [Ring R] [] {f : } :
theorem Polynomial.integralNormalization_eval₂_eq_zero {R : Type u} {S : Type v} [] [] [] {p : } (f : R →+* S) {z : S} (hz : = 0) (inj : ∀ (x : R), f x = 0x = 0) :
Polynomial.eval₂ f (z * f ()) () = 0
theorem Polynomial.integralNormalization_aeval_eq_zero {R : Type u} {S : Type v} [] [] [] [Algebra R S] {f : } {z : S} (hz : ↑() f = 0) (inj : ∀ (x : R), ↑() x = 0x = 0) :
↑(Polynomial.aeval (z * ↑() ())) () = 0