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

• One or more equations did not get rendered due to their size.

@[simp]

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

theorem Polynomial.integralNormalization_coeff {R : Type u} [Semiring R] {f : Polynomial R} {i : ℕ} : Polynomial.coeff (Polynomial.integralNormalization f) i = if Polynomial.degree f = ↑i then 1 else Polynomial.coeff f i * Polynomial.leadingCoeff f ^ (Polynomial.natDegree f - 1 - i)

theorem Polynomial.integralNormalization_support {R : Type u} [Semiring R] {f : Polynomial R} : Polynomial.support (Polynomial.integralNormalization f) ⊆ Polynomial.support f

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

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

theorem Polynomial.integralNormalization_coeff_ne_degree {R : Type u} [Semiring R] {f : Polynomial R} {i : ℕ} (hi : Polynomial.degree f ≠ ↑i) : Polynomial.coeff (Polynomial.integralNormalization f) i = Polynomial.coeff f i * Polynomial.leadingCoeff f ^ (Polynomial.natDegree f - 1 - i)

theorem Polynomial.integralNormalization_coeff_ne_natDegree {R : Type u} [Semiring R] {f : Polynomial R} {i : ℕ} (hi : i ≠ Polynomial.natDegree f) : Polynomial.coeff (Polynomial.integralNormalization f) i = Polynomial.coeff f i * Polynomial.leadingCoeff f ^ (Polynomial.natDegree f - 1 - i)

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

@[simp]

theorem Polynomial.support_integralNormalization {R : Type u} [Ring R] [IsDomain R] {f : Polynomial R} : Polynomial.support (Polynomial.integralNormalization f) = Polynomial.support f

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 = 0 → x = 0) : Polynomial.eval₂ f (z * ↑f (Polynomial.leadingCoeff p)) (Polynomial.integralNormalization p) = 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 = 0 → x = 0) : ↑(Polynomial.aeval (z * ↑(algebraMap R S) (Polynomial.leadingCoeff f))) (Polynomial.integralNormalization f) = 0