Theory of monic polynomials #
We define integralNormalization
, which relate arbitrary polynomials to monic ones.
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
Instances For
@[simp]
@[deprecated Polynomial.support_integralNormalization_subset (since := "2024-11-30")]
theorem
Polynomial.monic_integralNormalization
{R : Type u}
[Semiring R]
{p : Polynomial R}
(hp : p ≠ 0)
:
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'))
:
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)
:
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)
:
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)
: