Documentation

Mathlib.RingTheory.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 : R[X].

Main Results #

Note #

This has nothing to do with minimal polynomials of primitive elements in finite fields.

A polynomial is primitive when the only constant polynomials dividing it are units. Note: This has nothing to do with minimal polynomials of primitive elements in finite fields.

Equations
theorem Polynomial.isPrimitive_of_dvd {R : Type u_1} [CommSemiring R] {p q : Polynomial R} (hp : p.IsPrimitive) (hq : q p) :
theorem Irreducible.isPrimitive {R : Type u_1} [CommSemiring R] [NoZeroDivisors R] {p : Polynomial R} (hp : Irreducible p) (hp' : p.natDegree 0) :

An irreducible nonconstant polynomial over a domain is primitive.

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

Equations
@[simp]
theorem Polynomial.content_C {R : Type u_1} [CommRing R] [IsDomain R] [NormalizedGCDMonoid R] {r : R} :
@[simp]
theorem Polynomial.content_X_pow {R : Type u_1} [CommRing R] [IsDomain R] [NormalizedGCDMonoid R] {k : } :
(X ^ k).content = 1
@[simp]
theorem Polynomial.content_monomial {R : Type u_1} [CommRing R] [IsDomain R] [NormalizedGCDMonoid R] {r : R} {k : } :
noncomputable def Polynomial.primPart {R : Type u_1} [CommRing R] [IsDomain R] [NormalizedGCDMonoid 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.primPart = 1.

Equations
theorem Polynomial.aeval_primPart_eq_zero {R : Type u_1} [CommRing R] [IsDomain R] [NormalizedGCDMonoid R] {S : Type u_2} [Ring S] [IsDomain S] [Algebra R S] [NoZeroSMulDivisors R S] {p : Polynomial R} {s : S} (hpzero : p 0) (hp : (aeval s) p = 0) :
(aeval s) p.primPart = 0
theorem Polynomial.eval₂_primPart_eq_zero {R : Type u_1} [CommRing R] [IsDomain R] [NormalizedGCDMonoid R] {S : Type u_2} [CommSemiring S] [IsDomain S] {f : R →+* S} (hinj : Function.Injective f) {p : Polynomial R} {s : S} (hpzero : p 0) (hp : eval₂ f s p = 0) :
theorem Polynomial.gcd_content_eq_of_dvd_sub {R : Type u_1} [CommRing R] [IsDomain R] [NormalizedGCDMonoid R] {a : R} {p q : Polynomial R} (h : C a p - q) :
@[simp]
@[simp]
theorem Polynomial.primPart_mul {R : Type u_1} [CommRing R] [IsDomain R] [NormalizedGCDMonoid R] {p q : Polynomial R} (h0 : p * q 0) :
theorem Polynomial.exists_primitive_lcm_of_isPrimitive {R : Type u_1} [CommRing R] [IsDomain R] [NormalizedGCDMonoid R] {p q : Polynomial R} (hp : p.IsPrimitive) (hq : q.IsPrimitive) :
∃ (r : Polynomial R), r.IsPrimitive ∀ (s : Polynomial R), p s q s r s
theorem Polynomial.degree_gcd_le_left {R : Type u_1} [CommRing R] [IsDomain R] [NormalizedGCDMonoid R] {p : Polynomial R} (hp : p 0) (q : Polynomial R) :