# 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] :
integralNormalization 0 = 0
source
@[simp]
theorem Polynomial.integralNormalization_C {R : Type u} [Semiring R] {x : R} (hx : x ≠ 0) :
(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
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 * 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_of_commute {R : Type u} [Semiring R] {p : Polynomial R} {A : Type u_1} [Semiring A] (h : 1 ≤ p.natDegree) (f : R →+* A) (x : A) (h₁ : Commute (f p.leadingCoeff) x) (h₂ : ∀ {r r' : R}, Commute (f r) (f r')) :
eval₂ f (f p.leadingCoeff * x) p.integralNormalization = f p.leadingCoeff ^ (p.natDegree - 1) * eval₂ f x p
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) :
eval₂ f (f p.leadingCoeff * x) p.integralNormalization = f p.leadingCoeff ^ (p.natDegree - 1) * eval₂ f x p
source
theorem Polynomial.integralNormalization_eval₂_eq_zero_of_commute {R : Type u} [Semiring R] {A : Type u_1} [Semiring A] {p : Polynomial R} (f : R →+* A) {z : A} (hz : eval₂ f z p = 0) (h₁ : Commute (f p.leadingCoeff) z) (h₂ : ∀ {r r' : R}, Commute (f r) (f r')) (inj : ∀ (x : R), f x = 0 → x = 0) :
eval₂ f (f p.leadingCoeff * z) p.integralNormalization = 0
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 : eval₂ f z p = 0) (inj : ∀ (x : R), f x = 0 → x = 0) :
eval₂ f (f p.leadingCoeff * z) p.integralNormalization = 0
source
theorem Polynomial.integralNormalization_aeval_eq_zero {S : Type v} {A : Type u_1} [CommSemiring S] [Semiring A] [Algebra S A] {f : Polynomial S} {z : A} (hz : (aeval z) f = 0) (inj : ∀ (x : S), (algebraMap S A) x = 0 → x = 0) :
(aeval ((algebraMap S A) 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