Documentation

Mathlib.RingTheory.Polynomial.IntegralNormalization

Theory of monic polynomials #

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

source
noncomputable def Polynomial.integralNormalization {R : Type u} [Semiring R] (p : Polynomial R) :
Polynomial R

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

Moreover, integralNormalization 0 = 0.

Equations
  • p.integralNormalization = p.sum fun (i : ℕ) (a : R) => (Polynomial.monomial i) (if p.degree = ↑i then 1 else a * p.leadingCoeff ^ (p.natDegree - 1 - i))
Instances For
    source
    @[simp]
    theorem Polynomial.integralNormalization_zero {R : Type u} [Semiring R] :
    Polynomial.integralNormalization 0 = 0
    source
    @[simp]
    theorem Polynomial.integralNormalization_C {R : Type u} [Semiring R] {x : R} (hx : x ≠ 0) :
    (Polynomial.C x).integralNormalization = 1
    source
    theorem Polynomial.integralNormalization_coeff {R : Type u} [Semiring R] {p : Polynomial R} {i : ℕ} :
    p.integralNormalization.coeff i = if p.degree = ↑i then 1 else p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i)
    source
    theorem Polynomial.support_integralNormalization_subset {R : Type u} [Semiring R] {p : Polynomial R} :
    p.integralNormalization.support ⊆ p.support
    source
    @[deprecated Polynomial.support_integralNormalization_subset]
    theorem Polynomial.integralNormalization_support {R : Type u} [Semiring R] {p : Polynomial R} :
    p.integralNormalization.support ⊆ p.support

    Alias of Polynomial.support_integralNormalization_subset.

    source
    theorem Polynomial.integralNormalization_coeff_degree {R : Type u} [Semiring R] {p : Polynomial R} {i : ℕ} (hi : p.degree = ↑i) :
    p.integralNormalization.coeff i = 1
    source
    theorem Polynomial.integralNormalization_coeff_natDegree {R : Type u} [Semiring R] {p : Polynomial R} (hp : p ≠ 0) :
    p.integralNormalization.coeff p.natDegree = 1
    source
    theorem Polynomial.integralNormalization_coeff_degree_ne {R : Type u} [Semiring R] {p : Polynomial R} {i : ℕ} (hi : p.degree ≠ ↑i) :
    p.integralNormalization.coeff i = p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i)
    source
    theorem Polynomial.integralNormalization_coeff_ne_natDegree {R : Type u} [Semiring R] {p : Polynomial R} {i : ℕ} (hi : i ≠ p.natDegree) :
    p.integralNormalization.coeff i = p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i)
    source
    theorem Polynomial.monic_integralNormalization {R : Type u} [Semiring R] {p : Polynomial R} (hp : p ≠ 0) :
    p.integralNormalization.Monic
    source
    theorem Polynomial.integralNormalization_coeff_mul_leadingCoeff_pow {R : Type u} [Semiring R] {p : Polynomial R} (i : ℕ) (hp : 1 ≤ p.natDegree) :
    p.integralNormalization.coeff i * p.leadingCoeff ^ i = p.coeff i * p.leadingCoeff ^ (p.natDegree - 1)
    source
    theorem Polynomial.integralNormalization_mul_C_leadingCoeff {R : Type u} [Semiring R] (p : Polynomial R) :
    p.integralNormalization * Polynomial.C p.leadingCoeff = p.scaleRoots p.leadingCoeff
    source
    theorem Polynomial.integralNormalization_degree {R : Type u} [Semiring R] {p : Polynomial R} :
    p.integralNormalization.degree = p.degree
    source
    theorem Polynomial.leadingCoeff_smul_integralNormalization {S : Type v} [CommSemiring S] (p : Polynomial S) :
    p.leadingCoeff • p.integralNormalization = p.scaleRoots p.leadingCoeff
    source
    theorem Polynomial.integralNormalization_eval₂_leadingCoeff_mul {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [CommSemiring S] (h : 1 ≤ p.natDegree) (f : R →+* S) (x : S) :
    Polynomial.eval₂ f (f p.leadingCoeff * x) p.integralNormalization = f p.leadingCoeff ^ (p.natDegree - 1) * Polynomial.eval₂ f x p
    source
    theorem Polynomial.integralNormalization_eval₂_eq_zero {R : Type u} {S : Type v} [Semiring R] [CommSemiring S] {p : Polynomial R} (f : R →+* S) {z : S} (hz : Polynomial.eval₂ f z p = 0) (inj : ∀ (x : R), f x = 0 → x = 0) :
    Polynomial.eval₂ f (f p.leadingCoeff * z) p.integralNormalization = 0
    source
    theorem Polynomial.integralNormalization_aeval_eq_zero {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] [Algebra R S] {f : Polynomial R} {z : S} (hz : (Polynomial.aeval z) f = 0) (inj : ∀ (x : R), (algebraMap R S) x = 0 → x = 0) :
    (Polynomial.aeval ((algebraMap R S) f.leadingCoeff * z)) f.integralNormalization = 0
    source
    @[simp]
    theorem Polynomial.support_integralNormalization {R : Type u} [Semiring R] [IsCancelMulZero R] {f : Polynomial R} :
    f.integralNormalization.support = f.support