mathlib documentation

data.polynomial.integral_normalization

Theory of monic polynomials #

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

source
noncomputable def polynomial.integral_normalization {R : Type u} [semiring R] (f : R[X]) :
R[X]

If f : R[X] is a nonzero polynomial with root z, integral_normalization f is a monic polynomial with root leading_coeff f * z.

Moreover, integral_normalization 0 = 0.

Equations
source
@[simp]
theorem polynomial.integral_normalization_zero {R : Type u} [semiring R] :
0.integral_normalization = 0
source
theorem polynomial.integral_normalization_coeff {R : Type u} [semiring R] {f : R[X]} {i : ℕ} :
f.integral_normalization.coeff i = ite (f.degree = ↑i) 1 ((f.coeff i) * f.leading_coeff ^ (f.nat_degree - 1 - i))
source
theorem polynomial.integral_normalization_support {R : Type u} [semiring R] {f : R[X]} :
f.integral_normalization.support ⊆ f.support
source
theorem polynomial.integral_normalization_coeff_degree {R : Type u} [semiring R] {f : R[X]} {i : ℕ} (hi : f.degree = ↑i) :
f.integral_normalization.coeff i = 1
source
theorem polynomial.integral_normalization_coeff_nat_degree {R : Type u} [semiring R] {f : R[X]} (hf : f ≠ 0) :
f.integral_normalization.coeff f.nat_degree = 1
source
theorem polynomial.integral_normalization_coeff_ne_degree {R : Type u} [semiring R] {f : R[X]} {i : ℕ} (hi : f.degree ≠ ↑i) :
f.integral_normalization.coeff i = (f.coeff i) * f.leading_coeff ^ (f.nat_degree - 1 - i)
source
theorem polynomial.integral_normalization_coeff_ne_nat_degree {R : Type u} [semiring R] {f : R[X]} {i : ℕ} (hi : i ≠ f.nat_degree) :
f.integral_normalization.coeff i = (f.coeff i) * f.leading_coeff ^ (f.nat_degree - 1 - i)
source
theorem polynomial.monic_integral_normalization {R : Type u} [semiring R] {f : R[X]} (hf : f ≠ 0) :
f.integral_normalization.monic
source
@[simp]
theorem polynomial.support_integral_normalization {R : Type u} [ring R] [is_domain R] {f : R[X]} :
f.integral_normalization.support = f.support
source
theorem polynomial.integral_normalization_eval₂_eq_zero {R : Type u} {S : Type v} [comm_ring R] [is_domain R] [comm_semiring S] {p : R[X]} (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 p.leading_coeff) p.integral_normalization = 0
source
theorem polynomial.integral_normalization_aeval_eq_zero {R : Type u} {S : Type v} [comm_ring R] [is_domain R] [comm_semiring S] [algebra R S] {f : R[X]} {z : S} (hz : ⇑(polynomial.aeval z) f = 0) (inj : ∀ (x : R), ⇑(algebra_map R S) x = 0 → x = 0) :
⇑(polynomial.aeval (z * ⇑(algebra_map R S) f.leading_coeff)) f.integral_normalization = 0