mathlib documentation

ring_theory.polynomial.content

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].

Main Results #

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
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
def polynomial.content {R : Type u_1} [comm_ring R] [is_domain R] [normalized_gcd_monoid R] (p : polynomial R) :
R

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

Equations
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
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.is_primitive_of_dvd {R : Type u_1} [comm_ring R] [is_domain R] [normalized_gcd_monoid R] {p q : polynomial R} (hp : p.is_primitive) (hdvd : q ∣ p) :
q.is_primitive
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
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