10.3. Content and primitive part🔗

Every nonzero integer polynomial factors as a scalar (its content, the nonnegative gcd of the coefficients) times a primitive polynomial whose coefficients have gcd 1. These two operations are the integer analogue of normalizing to a monic polynomial over a field.

def

Hex.ZPoly.content (f : Hex.ZPoly) : Int
Hex.ZPoly.content (f : Hex.ZPoly) : Int

The nonnegative gcd of the coefficients of f.

def

Hex.ZPoly.primitivePart (f : Hex.ZPoly) : Hex.ZPoly
Hex.ZPoly.primitivePart (f : Hex.ZPoly) :
  Hex.ZPoly

Divide every coefficient by the content to obtain a primitive polynomial.

def

Hex.ZPoly.Primitive (f : Hex.ZPoly) : Prop
Hex.ZPoly.Primitive (f : Hex.ZPoly) : Prop

A ZPoly is primitive when its content is 1.

A related substitution, used when transferring a factor of a monic transform back to the original polynomial, scales the variable rather than the polynomial.

def

Hex.ZPoly.dilate (c : Int) (p : Hex.ZPoly) : Hex.ZPoly
Hex.ZPoly.dilate (c : Int)
  (p : Hex.ZPoly) : Hex.ZPoly

Substitute the variable X ↦ c * X: the i-th coefficient is multiplied by c ^ i.

On a monic transform c^(d-1) · core(X / c) (the polynomial built by toMonic), this is the inverse of the integer-scaling substitution: it maps a monic factor g of the transform to g(c · X), an integer multiple of the corresponding factor of core. Composing with primitivePart recovers the primitive integer factor of core. This is not the same as DensePoly.scale, which multiplies the whole polynomial by a constant.

theorem

Hex.ZPoly.coeff_dilate (c : Int) (p : Hex.ZPoly) (n : Nat) :
  Hex.DensePoly.coeff (Hex.ZPoly.dilate c p) n =
    c ^ n * Hex.DensePoly.coeff p n
Hex.ZPoly.coeff_dilate (c : Int)
  (p : Hex.ZPoly) (n : Nat) :
  Hex.DensePoly.coeff
      (Hex.ZPoly.dilate c p) n =
    c ^ n * Hex.DensePoly.coeff p n

The n-th coefficient of dilate c p is c ^ n times the n-th coefficient of p.

The unit polynomials are exactly the two constants 1 and -1, and this is a decidable predicate.

def

Hex.ZPoly.IsUnit (f : Hex.ZPoly) : Prop
Hex.ZPoly.IsUnit (f : Hex.ZPoly) : Prop

A ZPoly is a unit iff it is the constant polynomial 1 or -1.

theorem

Hex.ZPoly.isUnit_iff (f : Hex.ZPoly) :
  f.IsUnit ↔ f = Hex.DensePoly.C 1 ∨ f = Hex.DensePoly.C (-1)
Hex.ZPoly.isUnit_iff (f : Hex.ZPoly) :
  f.IsUnit ↔
    f = Hex.DensePoly.C 1 ∨
      f = Hex.DensePoly.C (-1)

The IsUnit predicate is exactly equality with the constant polynomial 1 or the constant polynomial -1.

10.3.1. Worked example: content and primitive part🔗

The block below builds f = 2 + 4x + 6x², reads off its content and primitive part, and checks the reconstruction law and a dilation.

open Hex Hex.DensePoly

namespace HexPolyZChapterContent

-- f = 2 + 4x + 6x²
private def f : ZPoly := ofCoeffs #[2, 4, 6]

-- The content is the nonnegative gcd of the
-- coefficients; the primitive part divides it out.
#guard ZPoly.content f = 2
#guard (ZPoly.primitivePart f).toArray.toList = [1, 2, 3]

-- Scaling the primitive part by the content
-- reconstructs f.
#guard scale (ZPoly.content f) (ZPoly.primitivePart f) = f

-- A polynomial whose coefficients are coprime is
-- already primitive: its content is 1.
#guard ZPoly.content (ofCoeffs #[1, 2, 3]) = 1

-- Dilation X ↦ 2·X scales coefficient i by 2ⁱ.
private def g : ZPoly := ofCoeffs #[1, 1, 1]
#guard (ZPoly.dilate 2 g).toArray.toList = [1, 2, 4]

end HexPolyZChapterContent