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]
.
p.content
is thegcd
of the coefficients ofp
.p.is_primitive
indicates thatp.content = 1
.
Main Results #
polynomial.content_mul
: Ifp q : R[X]
, then(p * q).content = p.content * q.content
.polynomial.normalized_gcd_monoid
: The polynomial ring of a GCD domain is itself a GCD domain.
A polynomial is primitive when the only constant polynomials dividing it are units
Equations
- p.is_primitive = ∀ (r : R), ⇑polynomial.C r ∣ p → is_unit r
theorem
polynomial.is_primitive_iff_is_unit_of_C_dvd
{R : Type u_1}
[comm_semiring R]
{p : polynomial R} :
p.is_primitive ↔ ∀ (r : R), ⇑polynomial.C r ∣ p → is_unit r
@[simp]
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
.
theorem
polynomial.content_dvd_coeff
{R : Type u_1}
[comm_ring R]
[is_domain R]
[normalized_gcd_monoid R]
{p : polynomial R}
(n : ℕ) :
@[simp]
theorem
polynomial.content_C
{R : Type u_1}
[comm_ring R]
[is_domain R]
[normalized_gcd_monoid R]
{r : R} :
@[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] :
theorem
polynomial.content_X_mul
{R : Type u_1}
[comm_ring R]
[is_domain R]
[normalized_gcd_monoid R]
{p : polynomial R} :
(polynomial.X * p).content = p.content
@[simp]
theorem
polynomial.content_X_pow
{R : Type u_1}
[comm_ring R]
[is_domain R]
[normalized_gcd_monoid R]
{k : ℕ} :
(polynomial.X ^ k).content = 1
@[simp]
theorem
polynomial.content_C_mul
{R : Type u_1}
[comm_ring R]
[is_domain R]
[normalized_gcd_monoid R]
(r : R)
(p : polynomial R) :
@[simp]
theorem
polynomial.content_monomial
{R : Type u_1}
[comm_ring R]
[is_domain R]
[normalized_gcd_monoid R]
{r : R}
{k : ℕ} :
theorem
polynomial.content_eq_zero_iff
{R : Type u_1}
[comm_ring R]
[is_domain R]
[normalized_gcd_monoid R]
{p : polynomial R} :
@[simp]
theorem
polynomial.normalize_content
{R : Type u_1}
[comm_ring R]
[is_domain R]
[normalized_gcd_monoid R]
{p : polynomial R} :
theorem
polynomial.content_eq_gcd_range_of_lt
{R : Type u_1}
[comm_ring R]
[is_domain R]
[normalized_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}
[comm_ring R]
[is_domain R]
[normalized_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}
[comm_ring R]
[is_domain R]
[normalized_gcd_monoid R]
(p : polynomial R) :
theorem
polynomial.dvd_content_iff_C_dvd
{R : Type u_1}
[comm_ring R]
[is_domain R]
[normalized_gcd_monoid R]
{p : polynomial R}
{r : R} :
theorem
polynomial.C_content_dvd
{R : Type u_1}
[comm_ring R]
[is_domain R]
[normalized_gcd_monoid R]
(p : polynomial R) :
⇑polynomial.C p.content ∣ p
theorem
polynomial.is_primitive_iff_content_eq_one
{R : Type u_1}
[comm_ring R]
[is_domain R]
[normalized_gcd_monoid R]
{p : polynomial R} :
p.is_primitive ↔ p.content = 1
theorem
polynomial.is_primitive.content_eq_one
{R : Type u_1}
[comm_ring R]
[is_domain R]
[normalized_gcd_monoid R]
{p : polynomial R}
(hp : p.is_primitive) :
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
- p.prim_part = ite (p = 0) 1 (classical.some _)
theorem
polynomial.eq_C_content_mul_prim_part
{R : Type u_1}
[comm_ring R]
[is_domain R]
[normalized_gcd_monoid R]
(p : polynomial R) :
@[simp]
theorem
polynomial.prim_part_zero
{R : Type u_1}
[comm_ring R]
[is_domain R]
[normalized_gcd_monoid R] :
theorem
polynomial.is_primitive_prim_part
{R : Type u_1}
[comm_ring R]
[is_domain R]
[normalized_gcd_monoid R]
(p : polynomial R) :
theorem
polynomial.content_prim_part
{R : Type u_1}
[comm_ring R]
[is_domain R]
[normalized_gcd_monoid R]
(p : polynomial R) :
theorem
polynomial.prim_part_ne_zero
{R : Type u_1}
[comm_ring R]
[is_domain R]
[normalized_gcd_monoid R]
(p : polynomial R) :
theorem
polynomial.nat_degree_prim_part
{R : Type u_1}
[comm_ring R]
[is_domain R]
[normalized_gcd_monoid R]
(p : polynomial R) :
@[simp]
theorem
polynomial.is_primitive.prim_part_eq
{R : Type u_1}
[comm_ring R]
[is_domain R]
[normalized_gcd_monoid R]
{p : polynomial R}
(hp : p.is_primitive) :
theorem
polynomial.is_unit_prim_part_C
{R : Type u_1}
[comm_ring R]
[is_domain R]
[normalized_gcd_monoid R]
(r : R) :
theorem
polynomial.prim_part_dvd
{R : Type u_1}
[comm_ring R]
[is_domain R]
[normalized_gcd_monoid R]
(p : polynomial R) :
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) :
⇑(polynomial.aeval s) p.prim_part = 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) :
polynomial.eval₂ f s p.prim_part = 0
theorem
polynomial.gcd_content_eq_of_dvd_sub
{R : Type u_1}
[comm_ring R]
[is_domain R]
[normalized_gcd_monoid R]
{a : R}
{p q : polynomial R}
(h : ⇑polynomial.C a ∣ p - q) :
gcd_monoid.gcd a p.content = gcd_monoid.gcd a q.content
theorem
polynomial.content_mul_aux
{R : Type u_1}
[comm_ring R]
[is_domain R]
[normalized_gcd_monoid R]
{p q : polynomial R} :
gcd_monoid.gcd (p * q).erase_lead.content p.leading_coeff = gcd_monoid.gcd (p.erase_lead * q).content p.leading_coeff
@[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) :
(p * 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.is_primitive_of_dvd
{R : Type u_1}
[comm_ring R]
[is_domain R]
[normalized_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}
[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]
noncomputable
def
polynomial.normalized_gcd_monoid
{R : Type u_1}
[comm_ring R]
[is_domain R]
[normalized_gcd_monoid R] :
Equations
- polynomial.normalized_gcd_monoid = normalized_gcd_monoid_of_exists_lcm polynomial.normalized_gcd_monoid._proof_3
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) :
(gcd_monoid.gcd p q).degree ≤ p.degree
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) :
(gcd_monoid.gcd p q).degree ≤ q.degree