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.content {R : Type u_1} [integral_domain R] [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} [integral_domain R] [gcd_monoid R] {p : polynomial R} (n : ) :

@[simp]
theorem polynomial.content_C {R : Type u_1} [integral_domain R] [gcd_monoid R] {r : R} :

@[simp]
theorem polynomial.content_zero {R : Type u_1} [integral_domain R] [gcd_monoid R] :

@[simp]
theorem polynomial.content_one {R : Type u_1} [integral_domain R] [gcd_monoid R] :

@[simp]
theorem polynomial.content_X_pow {R : Type u_1} [integral_domain R] [gcd_monoid R] {k : } :

@[simp]

theorem polynomial.content_C_mul {R : Type u_1} [integral_domain R] [gcd_monoid R] (r : R) (p : polynomial R) :

@[simp]
theorem polynomial.content_monomial {R : Type u_1} [integral_domain R] [gcd_monoid R] {r : R} {k : } :

theorem polynomial.content_eq_zero_iff {R : Type u_1} [integral_domain R] [gcd_monoid R] {p : polynomial R} :
p.content = 0 p = 0

@[simp]

theorem polynomial.content_eq_gcd_range_of_lt {R : Type u_1} [integral_domain R] [gcd_monoid R] (p : polynomial R) (n : ) (h : p.nat_degree < n) :

def polynomial.is_primitive {R : Type u_1} [integral_domain R] [gcd_monoid R] (p : polynomial R) :
Prop

A polynomial over a GCD domain is primitive when the gcd of its coefficients is 1

Equations
@[simp]

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

theorem polynomial.is_primitive.ne_zero {R : Type u_1} [integral_domain R] [gcd_monoid R] {p : polynomial R} (hp : p.is_primitive) :
p 0

def polynomial.prim_part {R : Type u_1} [integral_domain R] [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]
theorem polynomial.prim_part_zero {R : Type u_1} [integral_domain R] [gcd_monoid R] :

theorem polynomial.prim_part_ne_zero {R : Type u_1} [integral_domain R] [gcd_monoid R] (p : polynomial R) :

@[simp]
theorem polynomial.is_primitive.prim_part_eq {R : Type u_1} [integral_domain R] [gcd_monoid R] {p : polynomial R} (hp : p.is_primitive) :

theorem polynomial.prim_part_dvd {R : Type u_1} [integral_domain R] [gcd_monoid R] (p : polynomial R) :

theorem polynomial.gcd_content_eq_of_dvd_sub {R : Type u_1} [integral_domain R] [gcd_monoid R] {a : R} {p q : polynomial R} (h : polynomial.C a p - q) :

@[simp]
theorem polynomial.content_mul {R : Type u_1} [integral_domain R] [gcd_monoid R] {p q : polynomial R} :
(p * q).content = (p.content) * q.content

theorem polynomial.is_primitive.mul {R : Type u_1} [integral_domain R] [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} [integral_domain R] [gcd_monoid R] {p q : polynomial R} (h0 : p * q 0) :

theorem polynomial.is_primitive.is_primitive_of_dvd {R : Type u_1} [integral_domain R] [gcd_monoid R] {p q : polynomial R} (hp : p.is_primitive) (hdvd : q p) :

theorem polynomial.is_primitive.dvd_prim_part_iff_dvd {R : Type u_1} [integral_domain R] [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} [integral_domain R] [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

@[instance]

Equations