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 #

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
@[simp]
theorem polynomial.is_primitive_one {R : Type u_1} [comm_semiring R] :
theorem polynomial.monic.is_primitive {R : Type u_1} [comm_semiring R] {p : polynomial R} (hp : p.monic) :
theorem polynomial.is_primitive.ne_zero {R : Type u_1} [comm_semiring R] [nontrivial R] {p : polynomial R} (hp : p.is_primitive) :
p 0
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
theorem polynomial.content_dvd_coeff {R : Type u_1} [comm_ring R] [is_domain R] [normalized_gcd_monoid R] {p : polynomial R} (n : ) :
@[simp]
@[simp]
theorem polynomial.content_zero {R : Type u_1} [comm_ring R] [is_domain R] [normalized_gcd_monoid R] :
@[simp]
theorem polynomial.content_one {R : Type u_1} [comm_ring R] [is_domain R] [normalized_gcd_monoid R] :
@[simp]
theorem polynomial.content_X_pow {R : Type u_1} [comm_ring R] [is_domain R] [normalized_gcd_monoid R] {k : } :
@[simp]
@[simp]
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
noncomputable def polynomial.prim_part {R : Type u_1} [comm_ring R] [is_domain R] [normalized_gcd_monoid 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]
@[simp]
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) :
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) :
@[simp]
theorem polynomial.content_mul {R : Type u_1} [comm_ring R] [is_domain R] [normalized_gcd_monoid R] {p q : polynomial R} :
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) :
@[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) :
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) :
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
@[protected, instance]
Equations
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) :
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) :