Theory of monic polynomials

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

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))

@[simp]

theorem Polynomial.integralNormalization_zero {R : Type u} [Semiring R] : integralNormalization 0 = 0

@[simp]

theorem Polynomial.integralNormalization_C {R : Type u} [Semiring R] {x : R} (hx : x ≠ 0) : (C x).integralNormalization = 1

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)

theorem Polynomial.support_integralNormalization_subset {R : Type u} [Semiring R] {p : Polynomial R} : p.integralNormalization.support ⊆ p.support

theorem Polynomial.integralNormalization_coeff_degree {R : Type u} [Semiring R] {p : Polynomial R} {i : ℕ} (hi : p.degree = ↑i) : p.integralNormalization.coeff i = 1

theorem Polynomial.integralNormalization_coeff_natDegree {R : Type u} [Semiring R] {p : Polynomial R} (hp : p ≠ 0) : p.integralNormalization.coeff p.natDegree = 1

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)

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)

@[simp]

theorem Polynomial.degree_integralNormalization {R : Type u} [Semiring R] {p : Polynomial R} : p.integralNormalization.degree = p.degree

@[simp]

theorem Polynomial.natDegree_integralNormalization {R : Type u} [Semiring R] {p : Polynomial R} : p.integralNormalization.natDegree = p.natDegree

theorem Polynomial.monic_integralNormalization {R : Type u} [Semiring R] {p : Polynomial R} (hp : p ≠ 0) : p.integralNormalization.Monic

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)

theorem Polynomial.integralNormalization_mul_C_leadingCoeff {R : Type u} [Semiring R] (p : Polynomial R) : p.integralNormalization * C p.leadingCoeff = p.scaleRoots p.leadingCoeff

theorem Polynomial.leadingCoeff_smul_integralNormalization {S : Type v} [CommSemiring S] (p : Polynomial S) : p.leadingCoeff • p.integralNormalization = p.scaleRoots p.leadingCoeff

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

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

theorem Polynomial.integralNormalization_aeval_smul {S : Type v} [CommSemiring S] {R : Type u_2} [CommSemiring R] [Algebra R S] {p : Polynomial R} (h : 1 ≤ p.natDegree) (x : S) : (aeval (p.leadingCoeff • x)) p.integralNormalization = p.leadingCoeff ^ (p.natDegree - 1) • (aeval x) p

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

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

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

theorem Polynomial.integralNormalization_map {R : Type u} [Semiring R] {A : Type u_1} [Semiring A] (f : R →+* A) (p : Polynomial R) (H : f p.leadingCoeff ≠ 0) : (map f p).integralNormalization = map f p.integralNormalization

@[simp]

theorem Polynomial.support_integralNormalization {R : Type u} [Semiring R] [IsCancelMulZero R] {f : Polynomial R} : f.integralNormalization.support = f.support