# 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
• p.IsPrimitive = ∀ (r : R), Polynomial.C r p
Instances For
theorem Polynomial.isPrimitive_iff_isUnit_of_C_dvd {R : Type u_1} [] {p : } :
p.IsPrimitive ∀ (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 : p.Monic) :
p.IsPrimitive
theorem Polynomial.IsPrimitive.ne_zero {R : Type u_1} [] [] {p : } (hp : p.IsPrimitive) :
p 0
theorem Polynomial.isPrimitive_of_dvd {R : Type u_1} [] {p : } {q : } (hp : p.IsPrimitive) (hq : q p) :
q.IsPrimitive
def Polynomial.content {R : Type u_1} [] [] (p : ) :
R

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

Equations
• p.content = p.support.gcd p.coeff
Instances For
theorem Polynomial.content_dvd_coeff {R : Type u_1} [] [] {p : } (n : ) :
p.content p.coeff n
@[simp]
theorem Polynomial.content_C {R : Type u_1} [] [] {r : R} :
(Polynomial.C r).content = 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.X * p).content = p.content
@[simp]
theorem Polynomial.content_X_pow {R : Type u_1} [] [] {k : } :
(Polynomial.X ^ k).content = 1
@[simp]
theorem Polynomial.content_X {R : Type u_1} [] [] :
Polynomial.X.content = 1
theorem Polynomial.content_C_mul {R : Type u_1} [] [] (r : R) (p : ) :
(Polynomial.C r * p).content = normalize r * p.content
@[simp]
theorem Polynomial.content_monomial {R : Type u_1} [] [] {r : R} {k : } :
( r).content = normalize r
theorem Polynomial.content_eq_zero_iff {R : Type u_1} [] [] {p : } :
p.content = 0 p = 0
theorem Polynomial.normalize_content {R : Type u_1} [] [] {p : } :
normalize p.content = p.content
@[simp]
theorem Polynomial.normUnit_content {R : Type u_1} [] [] {p : } :
normUnit p.content = 1
theorem Polynomial.content_eq_gcd_range_of_lt {R : Type u_1} [] [] (p : ) (n : ) (h : p.natDegree < n) :
p.content = ().gcd p.coeff
theorem Polynomial.content_eq_gcd_range_succ {R : Type u_1} [] [] (p : ) :
p.content = (Finset.range p.natDegree.succ).gcd p.coeff
theorem Polynomial.content_eq_gcd_leadingCoeff_content_eraseLead {R : Type u_1} [] [] (p : ) :
theorem Polynomial.dvd_content_iff_C_dvd {R : Type u_1} [] [] {p : } {r : R} :
r p.content Polynomial.C r p
theorem Polynomial.C_content_dvd {R : Type u_1} [] [] (p : ) :
Polynomial.C p.content p
theorem Polynomial.isPrimitive_iff_content_eq_one {R : Type u_1} [] [] {p : } :
p.IsPrimitive p.content = 1
theorem Polynomial.IsPrimitive.content_eq_one {R : Type u_1} [] [] {p : } (hp : p.IsPrimitive) :
p.content = 1
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
• p.primPart = if p = 0 then 1 else
Instances For
theorem Polynomial.eq_C_content_mul_primPart {R : Type u_1} [] [] (p : ) :
p = Polynomial.C p.content * p.primPart
@[simp]
theorem Polynomial.primPart_zero {R : Type u_1} [] [] :
theorem Polynomial.isPrimitive_primPart {R : Type u_1} [] [] (p : ) :
p.primPart.IsPrimitive
theorem Polynomial.content_primPart {R : Type u_1} [] [] (p : ) :
p.primPart.content = 1
theorem Polynomial.primPart_ne_zero {R : Type u_1} [] [] (p : ) :
p.primPart 0
theorem Polynomial.natDegree_primPart {R : Type u_1} [] [] (p : ) :
p.primPart.natDegree = p.natDegree
@[simp]
theorem Polynomial.IsPrimitive.primPart_eq {R : Type u_1} [] [] {p : } (hp : p.IsPrimitive) :
p.primPart = p
theorem Polynomial.isUnit_primPart_C {R : Type u_1} [] [] (r : R) :
IsUnit (Polynomial.C r).primPart
theorem Polynomial.primPart_dvd {R : Type u_1} [] [] (p : ) :
p.primPart 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) :
() p.primPart = 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) :
Polynomial.eval₂ f s p.primPart = 0
theorem Polynomial.gcd_content_eq_of_dvd_sub {R : Type u_1} [] [] {a : R} {p : } {q : } (h : Polynomial.C a p - q) :
gcd a p.content = gcd a q.content
theorem Polynomial.content_mul_aux {R : Type u_1} [] [] {p : } {q : } :
@[simp]
theorem Polynomial.content_mul {R : Type u_1} [] [] {p : } {q : } :
(p * q).content = p.content * q.content
theorem Polynomial.IsPrimitive.mul {R : Type u_1} [] [] {p : } {q : } (hp : p.IsPrimitive) (hq : q.IsPrimitive) :
(p * q).IsPrimitive
@[simp]
theorem Polynomial.primPart_mul {R : Type u_1} [] [] {p : } {q : } (h0 : p * q 0) :
(p * q).primPart = p.primPart * q.primPart
theorem Polynomial.IsPrimitive.dvd_primPart_iff_dvd {R : Type u_1} [] [] {p : } {q : } (hp : p.IsPrimitive) (hq : q 0) :
p q.primPart p q
theorem Polynomial.exists_primitive_lcm_of_isPrimitive {R : Type u_1} [] [] {p : } {q : } (hp : p.IsPrimitive) (hq : q.IsPrimitive) :
∃ (r : ), r.IsPrimitive ∀ (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) :
p q p.content q.content p.primPart q.primPart
@[instance 100]
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 : ) :
(gcd p q).degree p.degree
theorem Polynomial.degree_gcd_le_right {R : Type u_1} [] [] (p : ) {q : } (hq : q 0) :
(gcd p q).degree q.degree