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
.
p.content
is thegcd
of the coefficients ofp
.p.is_primitive
indicates thatp.content = 1
.
Main Results #
polynomial.content_mul
: Ifp q : polynomial R
, then(p * q).content = p.content * q.content
.polynomial.gcd_monoid
: The polynomial ring of a GCD domain is itself a GCD domain.
p.content
is the gcd
of the coefficients of p
.
theorem
polynomial.content_dvd_coeff
{R : Type u_1}
[integral_domain R]
[gcd_monoid R]
{p : polynomial R}
(n : ℕ) :
@[simp]
@[simp]
@[simp]
theorem
polynomial.content_X_mul
{R : Type u_1}
[integral_domain R]
[gcd_monoid R]
{p : polynomial R} :
(polynomial.X * p).content = p.content
@[simp]
theorem
polynomial.content_X_pow
{R : Type u_1}
[integral_domain R]
[gcd_monoid R]
{k : ℕ} :
(polynomial.X ^ k).content = 1
@[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} :
@[simp]
theorem
polynomial.normalize_content
{R : Type u_1}
[integral_domain R]
[gcd_monoid R]
{p : polynomial R} :
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) :
p.content = (finset.range n).gcd p.coeff
theorem
polynomial.content_eq_gcd_range_succ
{R : Type u_1}
[integral_domain R]
[gcd_monoid R]
(p : polynomial R) :
p.content = (finset.range p.nat_degree.succ).gcd p.coeff
theorem
polynomial.content_eq_gcd_leading_coeff_content_erase_lead
{R : Type u_1}
[integral_domain R]
[gcd_monoid R]
(p : polynomial R) :
p.content = gcd p.leading_coeff p.erase_lead.content
theorem
polynomial.dvd_content_iff_C_dvd
{R : Type u_1}
[integral_domain R]
[gcd_monoid R]
{p : polynomial R}
{r : R} :
theorem
polynomial.C_content_dvd
{R : Type u_1}
[integral_domain R]
[gcd_monoid R]
(p : polynomial R) :
⇑polynomial.C p.content ∣ p
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
- p.is_primitive = (p.content = 1)
@[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
theorem
polynomial.is_primitive.content_eq_one
{R : Type u_1}
[integral_domain R]
[gcd_monoid R]
{p : polynomial R}
(hp : p.is_primitive) :
theorem
polynomial.is_primitive_iff_is_unit_of_C_dvd
{R : Type u_1}
[integral_domain R]
[gcd_monoid R]
{p : polynomial R} :
p.is_primitive ↔ ∀ (r : R), ⇑polynomial.C r ∣ p → is_unit 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
- p.prim_part = ite (p = 0) 1 (classical.some _)
theorem
polynomial.eq_C_content_mul_prim_part
{R : Type u_1}
[integral_domain R]
[gcd_monoid R]
(p : polynomial R) :
@[simp]
theorem
polynomial.is_primitive_prim_part
{R : Type u_1}
[integral_domain R]
[gcd_monoid R]
(p : polynomial R) :
theorem
polynomial.content_prim_part
{R : Type u_1}
[integral_domain R]
[gcd_monoid R]
(p : polynomial R) :
theorem
polynomial.prim_part_ne_zero
{R : Type u_1}
[integral_domain R]
[gcd_monoid R]
(p : polynomial R) :
theorem
polynomial.nat_degree_prim_part
{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) :
theorem
polynomial.content_mul_aux
{R : Type u_1}
[integral_domain R]
[gcd_monoid R]
{p q : polynomial R} :
gcd (p * q).erase_lead.content p.leading_coeff = gcd ((p.erase_lead) * q).content p.leading_coeff
@[simp]
theorem
polynomial.content_mul
{R : Type u_1}
[integral_domain R]
[gcd_monoid R]
{p q : polynomial R} :
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) :
(p * 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
theorem
polynomial.dvd_iff_content_dvd_content_and_prim_part_dvd_prim_part
{R : Type u_1}
[integral_domain R]
[gcd_monoid R]
{p q : polynomial R}
(hq : q ≠ 0) :
@[instance]
def
polynomial.gcd_monoid
{R : Type u_1}
[integral_domain R]
[gcd_monoid R] :
gcd_monoid (polynomial R)
Equations
- polynomial.gcd_monoid = gcd_monoid_of_exists_lcm polynomial.gcd_monoid._proof_5