mathlib3 documentation

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

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
theorem polynomial.is_primitive_of_dvd {R : Type u_1} [comm_semiring R] {p q : polynomial R} (hp : p.is_primitive) (hq : q p) :

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

Equations
@[simp]
@[simp]
@[simp]
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
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} :
@[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) :
@[protected, instance]
Equations