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 : polynomial R.

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] [integral_domain R] [normalized_gcd_monoid R] (p : polynomial R) :
R

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

Equations
@[simp]
@[simp]
@[simp]

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.content_mul {R : Type u_1} [comm_ring R] [integral_domain R] [normalized_gcd_monoid R] {p q : polynomial R} :
(p * q).content = (p.content) * q.content
@[simp]
theorem polynomial.prim_part_mul {R : Type u_1} [comm_ring R] [integral_domain R] [normalized_gcd_monoid R] {p q : polynomial R} (h0 : p * q 0) :
theorem polynomial.exists_primitive_lcm_of_is_primitive {R : Type u_1} [comm_ring R] [integral_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