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} [Semiring R] (f : Polynomial R) :

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.

Equations
  • f.integralNormalization = if.support, (Polynomial.monomial i) (if f.degree = i then 1 else f.coeff i * f.leadingCoeff ^ (f.natDegree - 1 - i))
Instances For
    theorem Polynomial.integralNormalization_coeff {R : Type u} [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)
    theorem Polynomial.integralNormalization_support {R : Type u} [Semiring R] {f : Polynomial R} :
    f.integralNormalization.support f.support
    theorem Polynomial.integralNormalization_coeff_degree {R : Type u} [Semiring R] {f : Polynomial R} {i : } (hi : f.degree = i) :
    f.integralNormalization.coeff i = 1
    theorem Polynomial.integralNormalization_coeff_natDegree {R : Type u} [Semiring R] {f : Polynomial R} (hf : f 0) :
    f.integralNormalization.coeff f.natDegree = 1
    theorem Polynomial.integralNormalization_coeff_ne_degree {R : Type u} [Semiring R] {f : Polynomial R} {i : } (hi : f.degree i) :
    f.integralNormalization.coeff i = f.coeff i * f.leadingCoeff ^ (f.natDegree - 1 - i)
    theorem Polynomial.integralNormalization_coeff_ne_natDegree {R : Type u} [Semiring R] {f : Polynomial R} {i : } (hi : i f.natDegree) :
    f.integralNormalization.coeff i = f.coeff i * f.leadingCoeff ^ (f.natDegree - 1 - i)
    theorem Polynomial.monic_integralNormalization {R : Type u} [Semiring R] {f : Polynomial R} (hf : f 0) :
    f.integralNormalization.Monic
    @[simp]
    theorem Polynomial.support_integralNormalization {R : Type u} [Ring R] [IsDomain R] {f : Polynomial R} :
    f.integralNormalization.support = f.support
    theorem Polynomial.integralNormalization_eval₂_eq_zero {R : Type u} {S : Type v} [CommRing R] [IsDomain R] [CommSemiring S] {p : Polynomial R} (f : R →+* S) {z : S} (hz : Polynomial.eval₂ f z p = 0) (inj : ∀ (x : R), f x = 0x = 0) :
    Polynomial.eval₂ f (z * f p.leadingCoeff) p.integralNormalization = 0
    theorem Polynomial.integralNormalization_aeval_eq_zero {R : Type u} {S : Type v} [CommRing R] [IsDomain R] [CommSemiring S] [Algebra R S] {f : Polynomial R} {z : S} (hz : (Polynomial.aeval z) f = 0) (inj : ∀ (x : R), (algebraMap R S) x = 0x = 0) :
    (Polynomial.aeval (z * (algebraMap R S) f.leadingCoeff)) f.integralNormalization = 0