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} [CommSemiring R] (p : Polynomial R) : Prop

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

Equations

• p.IsPrimitive = ∀ (r : R), Polynomial.C r ∣ p → IsUnit r

theorem Polynomial.isPrimitive_iff_isUnit_of_C_dvd {R : Type u_1} [CommSemiring R] {p : Polynomial R} : p.IsPrimitive ↔ ∀ (r : R), Polynomial.C r ∣ p → IsUnit r

@[simp]

theorem Polynomial.isPrimitive_one {R : Type u_1} [CommSemiring R] : Polynomial.IsPrimitive 1

theorem Polynomial.Monic.isPrimitive {R : Type u_1} [CommSemiring R] {p : Polynomial R} (hp : p.Monic) : p.IsPrimitive

theorem Polynomial.IsPrimitive.ne_zero {R : Type u_1} [CommSemiring R] [Nontrivial R] {p : Polynomial R} (hp : p.IsPrimitive) : p ≠ 0

theorem Polynomial.isPrimitive_of_dvd {R : Type u_1} [CommSemiring R] {p q : Polynomial R} (hp : p.IsPrimitive) (hq : q ∣ p) : q.IsPrimitive

def Polynomial.content {R : Type u_1} [CommRing R] [IsDomain R] [NormalizedGCDMonoid R] (p : Polynomial R) : R

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

Equations

• p.content = p.support.gcd p.coeff

theorem Polynomial.content_dvd_coeff {R : Type u_1} [CommRing R] [IsDomain R] [NormalizedGCDMonoid R] {p : Polynomial R} (n : ℕ) : p.content ∣ p.coeff n

@[simp]

theorem Polynomial.content_C {R : Type u_1} [CommRing R] [IsDomain R] [NormalizedGCDMonoid R] {r : R} : (Polynomial.C r).content = normalize r

@[simp]

theorem Polynomial.content_zero {R : Type u_1} [CommRing R] [IsDomain R] [NormalizedGCDMonoid R] : Polynomial.content 0 = 0

@[simp]

theorem Polynomial.content_one {R : Type u_1} [CommRing R] [IsDomain R] [NormalizedGCDMonoid R] : Polynomial.content 1 = 1

theorem Polynomial.content_X_mul {R : Type u_1} [CommRing R] [IsDomain R] [NormalizedGCDMonoid R] {p : Polynomial R} : (Polynomial.X * p).content = p.content

@[simp]

theorem Polynomial.content_X_pow {R : Type u_1} [CommRing R] [IsDomain R] [NormalizedGCDMonoid R] {k : ℕ} : (Polynomial.X ^ k).content = 1

@[simp]

theorem Polynomial.content_X {R : Type u_1} [CommRing R] [IsDomain R] [NormalizedGCDMonoid R] : Polynomial.X.content = 1

theorem Polynomial.content_C_mul {R : Type u_1} [CommRing R] [IsDomain R] [NormalizedGCDMonoid R] (r : R) (p : Polynomial R) : (Polynomial.C r * p).content = normalize r * p.content

@[simp]

theorem Polynomial.content_monomial {R : Type u_1} [CommRing R] [IsDomain R] [NormalizedGCDMonoid R] {r : R} {k : ℕ} : ((Polynomial.monomial k) r).content = normalize r

theorem Polynomial.content_eq_zero_iff {R : Type u_1} [CommRing R] [IsDomain R] [NormalizedGCDMonoid R] {p : Polynomial R} : p.content = 0 ↔ p = 0

theorem Polynomial.normalize_content {R : Type u_1} [CommRing R] [IsDomain R] [NormalizedGCDMonoid R] {p : Polynomial R} : normalize p.content = p.content

@[simp]

theorem Polynomial.normUnit_content {R : Type u_1} [CommRing R] [IsDomain R] [NormalizedGCDMonoid R] {p : Polynomial R} : normUnit p.content = 1

theorem Polynomial.content_eq_gcd_range_of_lt {R : Type u_1} [CommRing R] [IsDomain R] [NormalizedGCDMonoid R] (p : Polynomial R) (n : ℕ) (h : p.natDegree < n) : p.content = (Finset.range n).gcd p.coeff

theorem Polynomial.content_eq_gcd_range_succ {R : Type u_1} [CommRing R] [IsDomain R] [NormalizedGCDMonoid R] (p : Polynomial R) : p.content = (Finset.range p.natDegree.succ).gcd p.coeff

theorem Polynomial.content_eq_gcd_leadingCoeff_content_eraseLead {R : Type u_1} [CommRing R] [IsDomain R] [NormalizedGCDMonoid R] (p : Polynomial R) : p.content = gcd p.leadingCoeff p.eraseLead.content

theorem Polynomial.dvd_content_iff_C_dvd {R : Type u_1} [CommRing R] [IsDomain R] [NormalizedGCDMonoid R] {p : Polynomial R} {r : R} : r ∣ p.content ↔ Polynomial.C r ∣ p

theorem Polynomial.C_content_dvd {R : Type u_1} [CommRing R] [IsDomain R] [NormalizedGCDMonoid R] (p : Polynomial R) : Polynomial.C p.content ∣ p

theorem Polynomial.isPrimitive_iff_content_eq_one {R : Type u_1} [CommRing R] [IsDomain R] [NormalizedGCDMonoid R] {p : Polynomial R} : p.IsPrimitive ↔ p.content = 1

theorem Polynomial.IsPrimitive.content_eq_one {R : Type u_1} [CommRing R] [IsDomain R] [NormalizedGCDMonoid R] {p : Polynomial R} (hp : p.IsPrimitive) : p.content = 1

noncomputable def Polynomial.primPart {R : Type u_1} [CommRing R] [IsDomain R] [NormalizedGCDMonoid R] (p : Polynomial R) : Polynomial R

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 Classical.choose ⋯

theorem Polynomial.eq_C_content_mul_primPart {R : Type u_1} [CommRing R] [IsDomain R] [NormalizedGCDMonoid R] (p : Polynomial R) : p = Polynomial.C p.content * p.primPart

@[simp]

theorem Polynomial.primPart_zero {R : Type u_1} [CommRing R] [IsDomain R] [NormalizedGCDMonoid R] : Polynomial.primPart 0 = 1

theorem Polynomial.isPrimitive_primPart {R : Type u_1} [CommRing R] [IsDomain R] [NormalizedGCDMonoid R] (p : Polynomial R) : p.primPart.IsPrimitive

theorem Polynomial.content_primPart {R : Type u_1} [CommRing R] [IsDomain R] [NormalizedGCDMonoid R] (p : Polynomial R) : p.primPart.content = 1

theorem Polynomial.primPart_ne_zero {R : Type u_1} [CommRing R] [IsDomain R] [NormalizedGCDMonoid R] (p : Polynomial R) : p.primPart ≠ 0

theorem Polynomial.natDegree_primPart {R : Type u_1} [CommRing R] [IsDomain R] [NormalizedGCDMonoid R] (p : Polynomial R) : p.primPart.natDegree = p.natDegree

@[simp]

theorem Polynomial.IsPrimitive.primPart_eq {R : Type u_1} [CommRing R] [IsDomain R] [NormalizedGCDMonoid R] {p : Polynomial R} (hp : p.IsPrimitive) : p.primPart = p

theorem Polynomial.isUnit_primPart_C {R : Type u_1} [CommRing R] [IsDomain R] [NormalizedGCDMonoid R] (r : R) : IsUnit (Polynomial.C r).primPart

theorem Polynomial.primPart_dvd {R : Type u_1} [CommRing R] [IsDomain R] [NormalizedGCDMonoid R] (p : Polynomial R) : p.primPart ∣ p

theorem Polynomial.aeval_primPart_eq_zero {R : Type u_1} [CommRing R] [IsDomain R] [NormalizedGCDMonoid R] {S : Type u_2} [Ring S] [IsDomain S] [Algebra R S] [NoZeroSMulDivisors R S] {p : Polynomial R} {s : S} (hpzero : p ≠ 0) (hp : (Polynomial.aeval s) p = 0) : (Polynomial.aeval s) p.primPart = 0

theorem Polynomial.eval₂_primPart_eq_zero {R : Type u_1} [CommRing R] [IsDomain R] [NormalizedGCDMonoid R] {S : Type u_2} [CommRing S] [IsDomain S] {f : R →+* S} (hinj : Function.Injective ⇑f) {p : Polynomial R} {s : S} (hpzero : p ≠ 0) (hp : Polynomial.eval₂ f s p = 0) : Polynomial.eval₂ f s p.primPart = 0

theorem Polynomial.gcd_content_eq_of_dvd_sub {R : Type u_1} [CommRing R] [IsDomain R] [NormalizedGCDMonoid R] {a : R} {p q : Polynomial R} (h : Polynomial.C a ∣ p - q) : gcd a p.content = gcd a q.content

theorem Polynomial.content_mul_aux {R : Type u_1} [CommRing R] [IsDomain R] [NormalizedGCDMonoid R] {p q : Polynomial R} : gcd (p * q).eraseLead.content p.leadingCoeff = gcd (p.eraseLead * q).content p.leadingCoeff

@[simp]

theorem Polynomial.content_mul {R : Type u_1} [CommRing R] [IsDomain R] [NormalizedGCDMonoid R] {p q : Polynomial R} : (p * q).content = p.content * q.content

theorem Polynomial.IsPrimitive.mul {R : Type u_1} [CommRing R] [IsDomain R] [NormalizedGCDMonoid R] {p q : Polynomial R} (hp : p.IsPrimitive) (hq : q.IsPrimitive) : (p * q).IsPrimitive

@[simp]

theorem Polynomial.primPart_mul {R : Type u_1} [CommRing R] [IsDomain R] [NormalizedGCDMonoid R] {p q : Polynomial R} (h0 : p * q ≠ 0) : (p * q).primPart = p.primPart * q.primPart

theorem Polynomial.IsPrimitive.dvd_primPart_iff_dvd {R : Type u_1} [CommRing R] [IsDomain R] [NormalizedGCDMonoid R] {p q : Polynomial R} (hp : p.IsPrimitive) (hq : q ≠ 0) : p ∣ q.primPart ↔ p ∣ q

theorem Polynomial.exists_primitive_lcm_of_isPrimitive {R : Type u_1} [CommRing R] [IsDomain R] [NormalizedGCDMonoid R] {p q : Polynomial R} (hp : p.IsPrimitive) (hq : q.IsPrimitive) : ∃ (r : Polynomial R), r.IsPrimitive ∧ ∀ (s : Polynomial R), p ∣ s ∧ q ∣ s ↔ r ∣ s

theorem Polynomial.dvd_iff_content_dvd_content_and_primPart_dvd_primPart {R : Type u_1} [CommRing R] [IsDomain R] [NormalizedGCDMonoid R] {p q : Polynomial R} (hq : q ≠ 0) : p ∣ q ↔ p.content ∣ q.content ∧ p.primPart ∣ q.primPart

@[instance 100]

noncomputable instance Polynomial.normalizedGcdMonoid {R : Type u_1} [CommRing R] [IsDomain R] [NormalizedGCDMonoid R] : NormalizedGCDMonoid (Polynomial R)

Equations

• Polynomial.normalizedGcdMonoid = normalizedGCDMonoidOfExistsLCM ⋯

theorem Polynomial.degree_gcd_le_left {R : Type u_1} [CommRing R] [IsDomain R] [NormalizedGCDMonoid R] {p : Polynomial R} (hp : p ≠ 0) (q : Polynomial R) : (gcd p q).degree ≤ p.degree

theorem Polynomial.degree_gcd_le_right {R : Type u_1} [CommRing R] [IsDomain R] [NormalizedGCDMonoid R] (p : Polynomial R) {q : Polynomial R} (hq : q ≠ 0) : (gcd p q).degree ≤ q.degree