mathlib3documentation

ring_theory.polynomial.content

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.
def polynomial.is_primitive {R : Type u_1} (p : polynomial R) :
Prop

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

Equations
@[simp]
theorem polynomial.is_primitive_one {R : Type u_1}  :
theorem polynomial.monic.is_primitive {R : Type u_1} {p : polynomial R} (hp : p.monic) :
theorem polynomial.is_primitive.ne_zero {R : Type u_1} [nontrivial R] {p : polynomial R} (hp : p.is_primitive) :
p 0
theorem polynomial.is_primitive_of_dvd {R : Type u_1} {p q : polynomial R} (hp : p.is_primitive) (hq : q p) :
def polynomial.content {R : Type u_1} [comm_ring R] [is_domain R] (p : polynomial R) :
R

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

Equations
theorem polynomial.content_dvd_coeff {R : Type u_1} [comm_ring R] [is_domain R] {p : polynomial R} (n : ) :
@[simp]
theorem polynomial.content_C {R : Type u_1} [comm_ring R] [is_domain R] {r : R} :
@[simp]
theorem polynomial.content_zero {R : Type u_1} [comm_ring R] [is_domain R]  :
@[simp]
theorem polynomial.content_one {R : Type u_1} [comm_ring R] [is_domain R]  :
@[simp]
theorem polynomial.content_X_pow {R : Type u_1} [comm_ring R] [is_domain R] {k : } :
@[simp]
theorem polynomial.content_X {R : Type u_1} [comm_ring R] [is_domain R]  :
theorem polynomial.content_C_mul {R : Type u_1} [comm_ring R] [is_domain R] (r : R) (p : polynomial R) :
* p).content =
@[simp]
theorem polynomial.content_monomial {R : Type u_1} [comm_ring R] [is_domain R] {r : R} {k : } :
theorem polynomial.content_eq_zero_iff {R : Type u_1} [comm_ring R] [is_domain R] {p : polynomial R} :
p.content = 0 p = 0
@[simp]
theorem polynomial.normalize_content {R : Type u_1} [comm_ring R] [is_domain R] {p : polynomial R} :
theorem polynomial.dvd_content_iff_C_dvd {R : Type u_1} [comm_ring R] [is_domain R] {p : polynomial R} {r : R} :
theorem polynomial.C_content_dvd {R : Type u_1} [comm_ring R] [is_domain R] (p : polynomial R) :
noncomputable def polynomial.prim_part {R : Type u_1} [comm_ring R] [is_domain R] (p : 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
@[simp]
theorem polynomial.prim_part_zero {R : Type u_1} [comm_ring R] [is_domain R]  :
theorem polynomial.content_prim_part {R : Type u_1} [comm_ring R] [is_domain R] (p : polynomial R) :
@[simp]
theorem polynomial.is_unit_prim_part_C {R : Type u_1} [comm_ring R] [is_domain R] (r : R) :
theorem polynomial.prim_part_dvd {R : Type u_1} [comm_ring R] [is_domain R] (p : polynomial R) :
theorem polynomial.aeval_prim_part_eq_zero {R : Type u_1} [comm_ring R] [is_domain R] {S : Type u_2} [ring S] [is_domain S] [ S] {p : polynomial R} {s : S} (hpzero : p 0) (hp : p = 0) :
= 0
theorem polynomial.eval₂_prim_part_eq_zero {R : Type u_1} [comm_ring R] [is_domain 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 : p = 0) :
= 0
theorem polynomial.gcd_content_eq_of_dvd_sub {R : Type u_1} [comm_ring R] [is_domain R] {a : R} {p q : polynomial R} (h : p - q) :
theorem polynomial.content_mul_aux {R : Type u_1} [comm_ring R] [is_domain R] {p q : polynomial R} :
=
@[simp]
theorem polynomial.content_mul {R : Type u_1} [comm_ring R] [is_domain R] {p q : polynomial R} :
theorem polynomial.is_primitive.mul {R : Type u_1} [comm_ring R] [is_domain R] {p q : polynomial R} (hp : p.is_primitive) (hq : q.is_primitive) :
@[simp]
theorem polynomial.prim_part_mul {R : Type u_1} [comm_ring R] [is_domain R] {p q : polynomial R} (h0 : p * q 0) :
(p * q).prim_part =
theorem polynomial.is_primitive.dvd_prim_part_iff_dvd {R : Type u_1} [comm_ring R] [is_domain R] {p q : polynomial R} (hp : p.is_primitive) (hq : q 0) :
theorem polynomial.exists_primitive_lcm_of_is_primitive {R : Type u_1} [comm_ring R] [is_domain R] {p q : polynomial R} (hp : p.is_primitive) (hq : q.is_primitive) :
(r : , r.is_primitive (s : , p s q s r s
@[protected, instance]
noncomputable def polynomial.normalized_gcd_monoid {R : Type u_1} [comm_ring R] [is_domain R]  :
Equations
theorem polynomial.degree_gcd_le_left {R : Type u_1} [comm_ring R] [is_domain R] {p : polynomial R} (hp : p 0) (q : polynomial R) :
theorem polynomial.degree_gcd_le_right {R : Type u_1} [comm_ring R] [is_domain R] (p : polynomial R) {q : polynomial R} (hq : q 0) :