theorem Hex.ZPoly.primitiveSquareFreeDecomposition_primitive (f : ZPoly) : f.primitiveSquareFreeDecomposition.primitive = f.primitivePart

The primitive field of primitiveSquareFreeDecomposition f is the primitive part of f.

theorem Hex.ZPoly.leadingCoeff_normalizePrimitiveSign_nonneg (p : ZPoly) : 0 ≤ DensePoly.leadingCoeff p.normalizePrimitiveSign

Normalizing the primitive sign makes the leading coefficient nonnegative.

theorem Hex.ZPoly.leadingCoeff_ne_zero_of_ne_zero (p : ZPoly) (hp : p ≠ 0) : DensePoly.leadingCoeff p ≠ 0

A nonzero integer polynomial has nonzero leading coefficient.

theorem Hex.ZPoly.leadingCoeff_normalizePrimitiveSign_pos_of_ne_zero (p : ZPoly) (hp : p ≠ 0) : 0 < DensePoly.leadingCoeff p.normalizePrimitiveSign

Normalizing the primitive sign of a nonzero polynomial makes the leading coefficient positive.

theorem Hex.ZPoly.leadingCoeff_ratPolyPrimitivePart_nonneg (p : DensePoly Rat) : 0 ≤ DensePoly.leadingCoeff (ratPolyPrimitivePart p)

The rational primitive part has nonnegative integer leading coefficient.

theorem Hex.ZPoly.leadingCoeff_ratPolyPrimitivePart_pos_of_ne_zero (p : DensePoly Rat) (hp : p ≠ 0) : 0 < DensePoly.leadingCoeff (ratPolyPrimitivePart p)

The rational primitive part of a nonzero rational polynomial has positive integer leading coefficient.

theorem Hex.ZPoly.primitive_normalizePrimitiveSign {p : ZPoly} (hp : p.Primitive) : p.normalizePrimitiveSign.Primitive

Sign normalization preserves a primitive integer polynomial.

@[simp]

theorem Hex.ZPoly.size_normalizePrimitiveSign (p : ZPoly) : DensePoly.size p.normalizePrimitiveSign = DensePoly.size p

Sign normalization preserves the stored coefficient count.

@[simp]

theorem Hex.ZPoly.degree?_normalizePrimitiveSign (p : ZPoly) : DensePoly.degree? p.normalizePrimitiveSign = DensePoly.degree? p

Sign normalization preserves optional degree.

theorem Hex.ZPoly.ratPolyPrimitivePart_primitive (f : DensePoly Rat) (h : (ratPolyPrimitivePart f).content ≠ 0) : (ratPolyPrimitivePart f).Primitive

The rational primitive part is primitive when its content is nonzero.

theorem Hex.ZPoly.rational_associate_primitive_unit {p q : ZPoly} (hp : p.Primitive) (_hp_ne : p ≠ 0) (hq : q.Primitive) (_hq_ne : q ≠ 0) {unit : Rat} (hunit : p.toRatPoly = DensePoly.scale unit q.toRatPoly) : unit = 1 ∨ unit = -1

Gauss-style cancellation: if two primitive nonzero integer polynomials are rational associates with rational factor unit, then unit is ±1.

def Hex.ZPoly.reflectRat (p : DensePoly Rat) : DensePoly Rat

Substitute X ↦ -X in a rational dense polynomial. This local coefficient transform is the rational counterpart of ZPoly.dilate (-1).

Equations

• Hex.ZPoly.reflectRat p = Hex.DensePoly.ofList (List.map (fun (i : Nat) => (-1) ^ i * p.coeff i) (List.range p.size))

theorem Hex.ZPoly.coeff_reflectRat (p : DensePoly Rat) (n : Nat) : (reflectRat p).coeff n = (-1) ^ n * p.coeff n

Coefficients of rational reflection differ by the parity sign.

@[simp]

theorem Hex.ZPoly.size_reflectRat (p : DensePoly Rat) : (reflectRat p).size = p.size

Rational reflection preserves the stored coefficient count.

@[simp]

theorem Hex.ZPoly.reflectRat_reflectRat (p : DensePoly Rat) : reflectRat (reflectRat p) = p

Rational reflection is an involution.

theorem Hex.ZPoly.reflectRat_ne_zero {p : DensePoly Rat} (hp : p ≠ 0) : reflectRat p ≠ 0

Rational reflection preserves nonzeroness.

theorem Hex.ZPoly.derivative_reflectRat (p : DensePoly Rat) : (reflectRat p).derivative = DensePoly.scale (-1) (reflectRat p.derivative)

Differentiating a reflection contributes one global minus sign.

theorem Hex.ZPoly.reflectRat_mul (p q : DensePoly Rat) : reflectRat (p * q) = reflectRat p * reflectRat q

Rational reflection is multiplicative.

theorem Hex.ZPoly.reflectRat_dvd {p q : DensePoly Rat} (h : p ∣ q) : reflectRat p ∣ reflectRat q

Rational reflection transports polynomial divisibility.

theorem Hex.ZPoly.toRatPoly_dilate_neg_one (p : ZPoly) : (dilate (-1) p).toRatPoly = reflectRat p.toRatPoly

Casting an integer reflection to rational coefficients gives rational reflection.

theorem Hex.ZPoly.rat_size_scale {u : Rat} (hu : u ≠ 0) (p : DensePoly Rat) : (DensePoly.scale u p).size = p.size

Scaling a rational polynomial by a nonzero scalar preserves its size.

theorem Hex.ZPoly.rat_size_mul (f g : DensePoly Rat) (hf : f ≠ 0) (hg : g ≠ 0) : (f * g).size = f.size + g.size - 1

The size of a product of nonzero rational polynomials is one less than the sum of their sizes.

theorem Hex.ZPoly.rat_size_le_of_dvd_nonzero {d r : DensePoly Rat} (hd : d.size ≠ 0) (hr : r.size ≠ 0) : d ∣ r → d.size ≤ r.size

A nonzero rational polynomial divisor has size at most the size of the nonzero polynomial it divides.

instance Hex.ZPoly.instDivModLawsRat : DensePoly.DivModLaws Rat

theorem Hex.ZPoly.rat_mod_degree_lt (f g : DensePoly Rat) (h : 0 < g.natDegree) : (f % g).natDegree < g.natDegree

The rational remainder has degree below every positive-degree divisor. This direct wrapper lets downstream computational structures consume the public law without repeatedly elaborating the full typeclass dictionary.

theorem Hex.ZPoly.rat_mod_zpoly_degree_lt (f : DensePoly Rat) (p : ZPoly) (h : 0 < DensePoly.natDegree p) : (f % p.toRatPoly).natDegree < DensePoly.natDegree p

Remainder degree bound specialized to an integer polynomial cast to rational coefficients.

instance Hex.ZPoly.ratGcdLaws : DensePoly.GcdLaws Rat

theorem Hex.ZPoly.squareFreeRat_scale_neg_one (p : ZPoly) (h : p.SquareFreeRat) : SquareFreeRat (DensePoly.scale (-1) p)

Multiplication by -1 preserves executable rational squarefreeness.

theorem Hex.ZPoly.squareFreeRat_normalizePrimitiveSign (p : ZPoly) (h : p.SquareFreeRat) : p.normalizePrimitiveSign.SquareFreeRat

Sign normalization preserves executable rational squarefreeness.

theorem Hex.ZPoly.squareFreeRat_dilate_neg_one (p : ZPoly) (h : p.SquareFreeRat) : (dilate (-1) p).SquareFreeRat

Reflection in the origin preserves executable rational squarefreeness.