10.5. Content multiplicativity🔗

The defining laws of the content/primitive-part decomposition are its reconstruction identity and Gauss's lemma: content is multiplicative, and the primitive part of a product is the product of the primitive parts.

theorem

Hex.ZPoly.content_mul_primitivePart (f : Hex.ZPoly) :
  Hex.DensePoly.scale f.content f.primitivePart = f
Hex.ZPoly.content_mul_primitivePart
  (f : Hex.ZPoly) :
  Hex.DensePoly.scale f.content
      f.primitivePart =
    f

Scaling the primitive part by the content reconstructs the original integer polynomial.

theorem

Hex.ZPoly.content_dvd_coeff (f : Hex.ZPoly) (n : Nat) :
  f.content ∣ Hex.DensePoly.coeff f n
Hex.ZPoly.content_dvd_coeff
  (f : Hex.ZPoly) (n : Nat) :
  f.content ∣ Hex.DensePoly.coeff f n

The content of an integer polynomial divides every coefficient.

theorem

Hex.ZPoly.content_mul (p q : Hex.ZPoly) :
  (p * q).content = p.content * q.content
Hex.ZPoly.content_mul (p q : Hex.ZPoly) :
  (p * q).content = p.content * q.content

ZPoly-level wrapper for DensePoly.content_mul: the content of a product of integer polynomials is the product of their contents.

theorem

Hex.ZPoly.primitivePart_mul (p q : Hex.ZPoly) :
  (p * q).primitivePart = p.primitivePart * q.primitivePart
Hex.ZPoly.primitivePart_mul
  (p q : Hex.ZPoly) :
  (p * q).primitivePart =
    p.primitivePart * q.primitivePart

ZPoly-level wrapper for DensePoly.primitivePart_mul (Gauss's lemma): the primitive part of a product of integer polynomials is the product of their primitive parts.

theorem

Hex.ZPoly.primitive_mul (p q : Hex.ZPoly) (hp : p.Primitive)
  (hq : q.Primitive) : (p * q).Primitive
Hex.ZPoly.primitive_mul (p q : Hex.ZPoly)
  (hp : p.Primitive) (hq : q.Primitive) :
  (p * q).Primitive

The product of primitive integer polynomials is primitive.