Theory of monic polynomials
We define integral_normalization, which relate arbitrary polynomials to monic ones.
If f : polynomial R 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
- f.integral_normalization = finsupp.on_finset f.support (λ (i : ℕ), ite (f.degree = ↑i) 1 ((f.coeff i) * f.leading_coeff ^ (f.nat_degree - 1 - i))) _
theorem
polynomial.integral_normalization_coeff_degree
{R : Type u}
[semiring R]
{f : polynomial R}
{i : ℕ}
(hi : f.degree = ↑i) :
f.integral_normalization.coeff i = 1
theorem
polynomial.integral_normalization_coeff_nat_degree
{R : Type u}
[semiring R]
{f : polynomial R}
(hf : f ≠ 0) :
theorem
polynomial.integral_normalization_coeff_ne_degree
{R : Type u}
[semiring R]
{f : polynomial R}
{i : ℕ}
(hi : f.degree ≠ ↑i) :
f.integral_normalization.coeff i = (f.coeff i) * f.leading_coeff ^ (f.nat_degree - 1 - i)
theorem
polynomial.integral_normalization_coeff_ne_nat_degree
{R : Type u}
[semiring R]
{f : polynomial R}
{i : ℕ}
(hi : i ≠ f.nat_degree) :
f.integral_normalization.coeff i = (f.coeff i) * f.leading_coeff ^ (f.nat_degree - 1 - i)
theorem
polynomial.monic_integral_normalization
{R : Type u}
[semiring R]
{f : polynomial R}
(hf : f ≠ 0) :
@[simp]
theorem
polynomial.support_integral_normalization
{R : Type u}
[integral_domain R]
{f : polynomial R}
(hf : f ≠ 0) :
theorem
polynomial.integral_normalization_eval₂_eq_zero
{R : Type u}
{S : Type v}
[integral_domain R]
[comm_ring S]
{p : polynomial R}
(hp : p ≠ 0)
(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
theorem
polynomial.integral_normalization_aeval_eq_zero
{R : Type u}
{S : Type v}
[integral_domain R]
[comm_ring S]
[algebra R S]
{f : polynomial R}
(hf : f ≠ 0)
{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