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 #

A polynomial is primitive when the only constant polynomials dividing it are units

Equations
Instances For
    theorem Polynomial.isPrimitive_iff_isUnit_of_C_dvd {R : Type u_1} [CommSemiring R] {p : Polynomial R} :
    Polynomial.IsPrimitive p ∀ (r : R), Polynomial.C r pIsUnit r

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

    Equations
    Instances For
      @[simp]
      theorem Polynomial.content_C {R : Type u_1} [CommRing R] [IsDomain R] [NormalizedGCDMonoid R] {r : R} :
      Polynomial.content (Polynomial.C r) = normalize r
      @[simp]
      theorem Polynomial.content_X_pow {R : Type u_1} [CommRing R] [IsDomain R] [NormalizedGCDMonoid R] {k : } :
      Polynomial.content (Polynomial.X ^ k) = 1
      @[simp]
      theorem Polynomial.content_X {R : Type u_1} [CommRing R] [IsDomain R] [NormalizedGCDMonoid R] :
      Polynomial.content Polynomial.X = 1
      theorem Polynomial.content_C_mul {R : Type u_1} [CommRing R] [IsDomain R] [NormalizedGCDMonoid R] (r : R) (p : Polynomial R) :
      Polynomial.content (Polynomial.C r * p) = normalize r * Polynomial.content p
      @[simp]
      theorem Polynomial.content_monomial {R : Type u_1} [CommRing R] [IsDomain R] [NormalizedGCDMonoid R] {r : R} {k : } :
      theorem Polynomial.dvd_content_iff_C_dvd {R : Type u_1} [CommRing R] [IsDomain R] [NormalizedGCDMonoid R] {p : Polynomial R} {r : R} :
      r Polynomial.content p Polynomial.C r p
      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
      Instances For
        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 : (Polynomial.aeval s) p = 0) :
        theorem Polynomial.eval₂_primPart_eq_zero {R : Type u_1} [CommRing R] [IsDomain R] [NormalizedGCDMonoid R] {S : Type u_2} [CommRing S] [IsDomain S] {f : R →+* S} (hinj : Function.Injective f) {p : Polynomial R} {s : S} (hpzero : p 0) (hp : Polynomial.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 : Polynomial R} {q : Polynomial R} (h : Polynomial.C a p - q) :
        Equations