GCD structures on polynomials #

Definitions and basic results about polynomials over GCD domains, particularly their contents and primitive polynomials.

Main Definitions #

Let p : R[X].

• p.content is the gcd of the coefficients of p.
• p.IsPrimitive indicates that p.content = 1.

Main Results #

• Polynomial.content_mul: If p q : R[X], then (p * q).content = p.content * q.content.
• Polynomial.NormalizedGcdMonoid: The polynomial ring of a GCD domain is itself a GCD domain.
def Polynomial.IsPrimitive {R : Type u_1} [] (p : ) :

A polynomial is primitive when the only constant polynomials dividing it are units

Equations
• = ∀ (r : R), Polynomial.C r p
Instances For
theorem Polynomial.isPrimitive_iff_isUnit_of_C_dvd {R : Type u_1} [] {p : } :
∀ (r : R), Polynomial.C r p
@[simp]
theorem Polynomial.isPrimitive_one {R : Type u_1} [] :
theorem Polynomial.Monic.isPrimitive {R : Type u_1} [] {p : } (hp : ) :
theorem Polynomial.IsPrimitive.ne_zero {R : Type u_1} [] [] {p : } (hp : ) :
p 0
theorem Polynomial.isPrimitive_of_dvd {R : Type u_1} [] {p : } {q : } (hp : ) (hq : q p) :
def Polynomial.content {R : Type u_1} [] [] (p : ) :
R

p.content is the gcd of the coefficients of p.

Equations
Instances For
theorem Polynomial.content_dvd_coeff {R : Type u_1} [] [] {p : } (n : ) :
@[simp]
theorem Polynomial.content_C {R : Type u_1} [] [] {r : R} :
Polynomial.content (Polynomial.C r) = normalize r
@[simp]
theorem Polynomial.content_zero {R : Type u_1} [] [] :
@[simp]
theorem Polynomial.content_one {R : Type u_1} [] [] :
theorem Polynomial.content_X_mul {R : Type u_1} [] [] {p : } :
Polynomial.content (Polynomial.X * p) =
@[simp]
theorem Polynomial.content_X_pow {R : Type u_1} [] [] {k : } :
Polynomial.content (Polynomial.X ^ k) = 1
@[simp]
theorem Polynomial.content_X {R : Type u_1} [] [] :
Polynomial.content Polynomial.X = 1
theorem Polynomial.content_C_mul {R : Type u_1} [] [] (r : R) (p : ) :
Polynomial.content (Polynomial.C r * p) = normalize r *
@[simp]
theorem Polynomial.content_monomial {R : Type u_1} [] [] {r : R} {k : } :
= normalize r
theorem Polynomial.content_eq_zero_iff {R : Type u_1} [] [] {p : } :
p = 0
theorem Polynomial.normalize_content {R : Type u_1} [] [] {p : } :
normalize =
@[simp]
theorem Polynomial.normUnit_content {R : Type u_1} [] [] {p : } :
theorem Polynomial.content_eq_gcd_range_of_lt {R : Type u_1} [] [] (p : ) (n : ) (h : ) :
theorem Polynomial.content_eq_gcd_range_succ {R : Type u_1} [] [] (p : ) :
theorem Polynomial.dvd_content_iff_C_dvd {R : Type u_1} [] [] {p : } {r : R} :
Polynomial.C r p
theorem Polynomial.C_content_dvd {R : Type u_1} [] [] (p : ) :
Polynomial.C p
theorem Polynomial.isPrimitive_iff_content_eq_one {R : Type u_1} [] [] {p : } :
theorem Polynomial.IsPrimitive.content_eq_one {R : Type u_1} [] [] {p : } (hp : ) :
noncomputable def Polynomial.primPart {R : Type u_1} [] [] (p : ) :

The primitive part of a polynomial p is the primitive polynomial gained by dividing p by p.content. If p = 0, then p.primPart = 1.

Equations
• = if p = 0 then 1 else
Instances For
theorem Polynomial.eq_C_content_mul_primPart {R : Type u_1} [] [] (p : ) :
p = Polynomial.C *
@[simp]
theorem Polynomial.primPart_zero {R : Type u_1} [] [] :
theorem Polynomial.isPrimitive_primPart {R : Type u_1} [] [] (p : ) :
theorem Polynomial.content_primPart {R : Type u_1} [] [] (p : ) :
theorem Polynomial.primPart_ne_zero {R : Type u_1} [] [] (p : ) :
theorem Polynomial.natDegree_primPart {R : Type u_1} [] [] (p : ) :
@[simp]
theorem Polynomial.IsPrimitive.primPart_eq {R : Type u_1} [] [] {p : } (hp : ) :
theorem Polynomial.isUnit_primPart_C {R : Type u_1} [] [] (r : R) :
IsUnit (Polynomial.primPart (Polynomial.C r))
theorem Polynomial.primPart_dvd {R : Type u_1} [] [] (p : ) :
theorem Polynomial.aeval_primPart_eq_zero {R : Type u_1} [] [] {S : Type u_2} [Ring S] [] [Algebra R S] [] {p : } {s : S} (hpzero : p 0) (hp : () p = 0) :
= 0
theorem Polynomial.eval₂_primPart_eq_zero {R : Type u_1} [] [] {S : Type u_2} [] [] {f : R →+* S} (hinj : ) {p : } {s : S} (hpzero : p 0) (hp : = 0) :
= 0
theorem Polynomial.gcd_content_eq_of_dvd_sub {R : Type u_1} [] [] {a : R} {p : } {q : } (h : Polynomial.C a p - q) :
=
theorem Polynomial.content_mul_aux {R : Type u_1} [] [] {p : } {q : } :
=
@[simp]
theorem Polynomial.content_mul {R : Type u_1} [] [] {p : } {q : } :
theorem Polynomial.IsPrimitive.mul {R : Type u_1} [] [] {p : } {q : } (hp : ) (hq : ) :
@[simp]
theorem Polynomial.primPart_mul {R : Type u_1} [] [] {p : } {q : } (h0 : p * q 0) :
theorem Polynomial.IsPrimitive.dvd_primPart_iff_dvd {R : Type u_1} [] [] {p : } {q : } (hp : ) (hq : q 0) :
p q
theorem Polynomial.exists_primitive_lcm_of_isPrimitive {R : Type u_1} [] [] {p : } {q : } (hp : ) (hq : ) :
∃ (r : ), ∀ (s : ), p s q s r s
theorem Polynomial.dvd_iff_content_dvd_content_and_primPart_dvd_primPart {R : Type u_1} [] [] {p : } {q : } (hq : q 0) :
noncomputable instance Polynomial.normalizedGcdMonoid {R : Type u_1} [] [] :
Equations
• Polynomial.normalizedGcdMonoid =
theorem Polynomial.degree_gcd_le_left {R : Type u_1} [] [] {p : } (hp : p 0) (q : ) :
theorem Polynomial.degree_gcd_le_right {R : Type u_1} [] [] (p : ) {q : } (hq : q 0) :