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

• Polynomial.IsPrimitive p = ∀ (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} : Polynomial.IsPrimitive p ↔ ∀ (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 : Polynomial.Monic p) : Polynomial.IsPrimitive p

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

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

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

• Polynomial.content p = Finset.gcd (Polynomial.support p) (Polynomial.coeff p)

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

@[simp]

theorem Polynomial.content_C {R : Type u_1} [CommRing R] [IsDomain R] [NormalizedGCDMonoid R] {r : R} : Polynomial.content (↑Polynomial.C r) = ↑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.content (Polynomial.X * p) = Polynomial.content p

@[simp]

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

@[simp]

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

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

@[simp]

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

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

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

@[simp]

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

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

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

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

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

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

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

theorem Polynomial.IsPrimitive.content_eq_one {R : Type u_1} [CommRing R] [IsDomain R] [NormalizedGCDMonoid R] {p : Polynomial R} (hp : Polynomial.IsPrimitive p) : Polynomial.content p = 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

• Polynomial.primPart p = if p = 0 then 1 else Classical.choose (_ : ↑Polynomial.C (Polynomial.content p) ∣ p)

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

@[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) : Polynomial.IsPrimitive (Polynomial.primPart p)

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

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

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

@[simp]

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

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

theorem Polynomial.primPart_dvd {R : Type u_1} [CommRing R] [IsDomain R] [NormalizedGCDMonoid R] (p : Polynomial R) : Polynomial.primPart p ∣ 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) (Polynomial.primPart p) = 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 (Polynomial.primPart p) = 0

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

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

@[simp]

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

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

@[simp]

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

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

theorem Polynomial.exists_primitive_lcm_of_isPrimitive {R : Type u_1} [CommRing R] [IsDomain R] [NormalizedGCDMonoid R] {p : Polynomial R} {q : Polynomial R} (hp : Polynomial.IsPrimitive p) (hq : Polynomial.IsPrimitive q) : ∃ r, Polynomial.IsPrimitive r ∧ ∀ (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 : Polynomial R} {q : Polynomial R} (hq : q ≠ 0) : p ∣ q ↔ Polynomial.content p ∣ Polynomial.content q ∧ Polynomial.primPart p ∣ Polynomial.primPart q

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

Equations

• Polynomial.normalizedGcdMonoid = normalizedGCDMonoidOfExistsLCM (_ : ∀ (p q : Polynomial R), ∃ c, ∀ (d : Polynomial R), p ∣ d ∧ q ∣ d ↔ c ∣ d)

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) : Polynomial.degree (gcd p q) ≤ Polynomial.degree p

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) : Polynomial.degree (gcd p q) ≤ Polynomial.degree q