GCD structures on polynomials #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.is_primitive indicates that p.content = 1.

Main Results #

polynomial.content_mul: If p q : R[X], then (p * q).content = p.content * q.content.
polynomial.normalized_gcd_monoid: The polynomial ring of a GCD domain is itself a GCD domain.

source

def polynomial.is_primitive {R : Type u_1} [comm_semiring R] (p : polynomial R) :

Prop

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

Equations

p.is_primitive = ∀ (r : R), ⇑polynomial.C r ∣ p → is_unit r

source

theorem polynomial.is_primitive_iff_is_unit_of_C_dvd {R : Type u_1} [comm_semiring R] {p : polynomial R} :

p.is_primitive ↔ ∀ (r : R), ⇑polynomial.C r ∣ p → is_unit r

source

@[simp]

theorem polynomial.is_primitive_one {R : Type u_1} [comm_semiring R] :

1.is_primitive

source

theorem polynomial.monic.is_primitive {R : Type u_1} [comm_semiring R] {p : polynomial R} (hp : p.monic) :

p.is_primitive

source

theorem polynomial.is_primitive.ne_zero {R : Type u_1} [comm_semiring R] [nontrivial R] {p : polynomial R} (hp : p.is_primitive) :

p ≠ 0

source

theorem polynomial.is_primitive_of_dvd {R : Type u_1} [comm_semiring R] {p q : polynomial R} (hp : p.is_primitive) (hq : q ∣ p) :

q.is_primitive

source

def polynomial.content {R : Type u_1} [comm_ring R] [is_domain R] [normalized_gcd_monoid R] (p : polynomial R) :

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

Equations

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

source

theorem polynomial.content_dvd_coeff {R : Type u_1} [comm_ring R] [is_domain R] [normalized_gcd_monoid R] {p : polynomial R} (n : ℕ) :

p.content ∣ p.coeff n

source

@[simp]

theorem polynomial.content_C {R : Type u_1} [comm_ring R] [is_domain R] [normalized_gcd_monoid R] {r : R} :

(⇑polynomial.C r).content = ⇑normalize r

source

@[simp]

theorem polynomial.content_zero {R : Type u_1} [comm_ring R] [is_domain R] [normalized_gcd_monoid R] :

0.content = 0

source

@[simp]

theorem polynomial.content_one {R : Type u_1} [comm_ring R] [is_domain R] [normalized_gcd_monoid R] :

1.content = 1

source

theorem polynomial.content_X_mul {R : Type u_1} [comm_ring R] [is_domain R] [normalized_gcd_monoid R] {p : polynomial R} :

(polynomial.X * p).content = p.content

source

@[simp]

theorem polynomial.content_X_pow {R : Type u_1} [comm_ring R] [is_domain R] [normalized_gcd_monoid R] {k : ℕ} :

(polynomial.X ^ k).content = 1

source

@[simp]

theorem polynomial.content_X {R : Type u_1} [comm_ring R] [is_domain R] [normalized_gcd_monoid R] :

polynomial.X.content = 1

source

theorem polynomial.content_C_mul {R : Type u_1} [comm_ring R] [is_domain R] [normalized_gcd_monoid R] (r : R) (p : polynomial R) :

(⇑polynomial.C r * p).content = ⇑normalize r * p.content

source

@[simp]

theorem polynomial.content_monomial {R : Type u_1} [comm_ring R] [is_domain R] [normalized_gcd_monoid R] {r : R} {k : ℕ} :

(⇑(polynomial.monomial k) r).content = ⇑normalize r

source

theorem polynomial.content_eq_zero_iff {R : Type u_1} [comm_ring R] [is_domain R] [normalized_gcd_monoid R] {p : polynomial R} :

p.content = 0 ↔ p = 0

source

@[simp]

theorem polynomial.normalize_content {R : Type u_1} [comm_ring R] [is_domain R] [normalized_gcd_monoid R] {p : polynomial R} :

⇑normalize p.content = p.content

source

theorem polynomial.content_eq_gcd_range_of_lt {R : Type u_1} [comm_ring R] [is_domain R] [normalized_gcd_monoid R] (p : polynomial R) (n : ℕ) (h : p.nat_degree < n) :

p.content = (finset.range n).gcd p.coeff

source

theorem polynomial.content_eq_gcd_range_succ {R : Type u_1} [comm_ring R] [is_domain R] [normalized_gcd_monoid R] (p : polynomial R) :

p.content = (finset.range p.nat_degree.succ).gcd p.coeff

source

theorem polynomial.content_eq_gcd_leading_coeff_content_erase_lead {R : Type u_1} [comm_ring R] [is_domain R] [normalized_gcd_monoid R] (p : polynomial R) :

p.content = gcd_monoid.gcd p.leading_coeff p.erase_lead.content

source

theorem polynomial.dvd_content_iff_C_dvd {R : Type u_1} [comm_ring R] [is_domain R] [normalized_gcd_monoid R] {p : polynomial R} {r : R} :

r ∣ p.content ↔ ⇑polynomial.C r ∣ p

source

theorem polynomial.C_content_dvd {R : Type u_1} [comm_ring R] [is_domain R] [normalized_gcd_monoid R] (p : polynomial R) :

⇑polynomial.C p.content ∣ p

source

theorem polynomial.is_primitive_iff_content_eq_one {R : Type u_1} [comm_ring R] [is_domain R] [normalized_gcd_monoid R] {p : polynomial R} :

p.is_primitive ↔ p.content = 1

source

theorem polynomial.is_primitive.content_eq_one {R : Type u_1} [comm_ring R] [is_domain R] [normalized_gcd_monoid R] {p : polynomial R} (hp : p.is_primitive) :

p.content = 1

source

noncomputable def polynomial.prim_part {R : Type u_1} [comm_ring R] [is_domain R] [normalized_gcd_monoid 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.prim_part = 1.

Equations

p.prim_part = ite (p = 0) 1 (classical.some _)

source

theorem polynomial.eq_C_content_mul_prim_part {R : Type u_1} [comm_ring R] [is_domain R] [normalized_gcd_monoid R] (p : polynomial R) :

p = ⇑polynomial.C p.content * p.prim_part

source

@[simp]

theorem polynomial.prim_part_zero {R : Type u_1} [comm_ring R] [is_domain R] [normalized_gcd_monoid R] :

0.prim_part = 1

source

theorem polynomial.is_primitive_prim_part {R : Type u_1} [comm_ring R] [is_domain R] [normalized_gcd_monoid R] (p : polynomial R) :

p.prim_part.is_primitive

source

theorem polynomial.content_prim_part {R : Type u_1} [comm_ring R] [is_domain R] [normalized_gcd_monoid R] (p : polynomial R) :

p.prim_part.content = 1

source

theorem polynomial.prim_part_ne_zero {R : Type u_1} [comm_ring R] [is_domain R] [normalized_gcd_monoid R] (p : polynomial R) :

p.prim_part ≠ 0

source

theorem polynomial.nat_degree_prim_part {R : Type u_1} [comm_ring R] [is_domain R] [normalized_gcd_monoid R] (p : polynomial R) :

p.prim_part.nat_degree = p.nat_degree

source

@[simp]

theorem polynomial.is_primitive.prim_part_eq {R : Type u_1} [comm_ring R] [is_domain R] [normalized_gcd_monoid R] {p : polynomial R} (hp : p.is_primitive) :

p.prim_part = p

source

theorem polynomial.is_unit_prim_part_C {R : Type u_1} [comm_ring R] [is_domain R] [normalized_gcd_monoid R] (r : R) :

is_unit (⇑polynomial.C r).prim_part

source

theorem polynomial.prim_part_dvd {R : Type u_1} [comm_ring R] [is_domain R] [normalized_gcd_monoid R] (p : polynomial R) :

p.prim_part ∣ p

source

theorem polynomial.aeval_prim_part_eq_zero {R : Type u_1} [comm_ring R] [is_domain R] [normalized_gcd_monoid R] {S : Type u_2} [ring S] [is_domain S] [algebra R S] [no_zero_smul_divisors R S] {p : polynomial R} {s : S} (hpzero : p ≠ 0) (hp : ⇑(polynomial.aeval s) p = 0) :

⇑(polynomial.aeval s) p.prim_part = 0

source

theorem polynomial.eval₂_prim_part_eq_zero {R : Type u_1} [comm_ring R] [is_domain R] [normalized_gcd_monoid R] {S : Type u_2} [comm_ring S] [is_domain 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.prim_part = 0

source

theorem polynomial.gcd_content_eq_of_dvd_sub {R : Type u_1} [comm_ring R] [is_domain R] [normalized_gcd_monoid R] {a : R} {p q : polynomial R} (h : ⇑polynomial.C a ∣ p - q) :

gcd_monoid.gcd a p.content = gcd_monoid.gcd a q.content

source

theorem polynomial.content_mul_aux {R : Type u_1} [comm_ring R] [is_domain R] [normalized_gcd_monoid R] {p q : polynomial R} :

gcd_monoid.gcd (p * q).erase_lead.content p.leading_coeff = gcd_monoid.gcd (p.erase_lead * q).content p.leading_coeff

source

@[simp]

theorem polynomial.content_mul {R : Type u_1} [comm_ring R] [is_domain R] [normalized_gcd_monoid R] {p q : polynomial R} :

(p * q).content = p.content * q.content

source

theorem polynomial.is_primitive.mul {R : Type u_1} [comm_ring R] [is_domain R] [normalized_gcd_monoid R] {p q : polynomial R} (hp : p.is_primitive) (hq : q.is_primitive) :

(p * q).is_primitive

source

@[simp]

theorem polynomial.prim_part_mul {R : Type u_1} [comm_ring R] [is_domain R] [normalized_gcd_monoid R] {p q : polynomial R} (h0 : p * q ≠ 0) :

(p * q).prim_part = p.prim_part * q.prim_part

source

theorem polynomial.is_primitive.dvd_prim_part_iff_dvd {R : Type u_1} [comm_ring R] [is_domain R] [normalized_gcd_monoid R] {p q : polynomial R} (hp : p.is_primitive) (hq : q ≠ 0) :

p ∣ q.prim_part ↔ p ∣ q

source

theorem polynomial.exists_primitive_lcm_of_is_primitive {R : Type u_1} [comm_ring R] [is_domain R] [normalized_gcd_monoid R] {p q : polynomial R} (hp : p.is_primitive) (hq : q.is_primitive) :

∃ (r : polynomial R), r.is_primitive ∧ ∀ (s : polynomial R), p ∣ s ∧ q ∣ s ↔ r ∣ s

source

theorem polynomial.dvd_iff_content_dvd_content_and_prim_part_dvd_prim_part {R : Type u_1} [comm_ring R] [is_domain R] [normalized_gcd_monoid R] {p q : polynomial R} (hq : q ≠ 0) :

p ∣ q ↔ p.content ∣ q.content ∧ p.prim_part ∣ q.prim_part

source

@[protected, instance]

noncomputable def polynomial.normalized_gcd_monoid {R : Type u_1} [comm_ring R] [is_domain R] [normalized_gcd_monoid R] :

normalized_gcd_monoid (polynomial R)

Equations

polynomial.normalized_gcd_monoid = normalized_gcd_monoid_of_exists_lcm polynomial.normalized_gcd_monoid._proof_3

source

theorem polynomial.degree_gcd_le_left {R : Type u_1} [comm_ring R] [is_domain R] [normalized_gcd_monoid R] {p : polynomial R} (hp : p ≠ 0) (q : polynomial R) :

(gcd_monoid.gcd p q).degree ≤ p.degree

source

theorem polynomial.degree_gcd_le_right {R : Type u_1} [comm_ring R] [is_domain R] [normalized_gcd_monoid R] (p : polynomial R) {q : polynomial R} (hq : q ≠ 0) :

(gcd_monoid.gcd p q).degree ≤ q.degree