theorem Hex.ZPoly.ne_zero_of_primitive (p : ZPoly) (hp : p.Primitive) : p ≠ 0

A primitive integer polynomial is nonzero.

theorem Hex.ZPoly.primitiveSquareFreeDecomposition_reassembly_over_rat (f : ZPoly) : have d := f.primitiveSquareFreeDecomposition; ∃ (unit : Rat), d.primitive.toRatPoly = DensePoly.scale unit (d.squareFreeCore.toRatPoly * d.repeatedPart.toRatPoly)

The primitive field reassembles over Rat[x] as a rational scalar multiple of the product of the square-free part and repeated part.

theorem Hex.ZPoly.primitiveSquareFreeDecomposition_squareFreeCore (f : ZPoly) (hcore : f.primitiveSquareFreeDecomposition.squareFreeCore ≠ 0) : f.primitiveSquareFreeDecomposition.squareFreeCore.SquareFreeRat

A nonzero square-free part from the primitive square-free decomposition is square-free over Rat[x].

theorem Hex.ZPoly.primitiveSquareFreeDecomposition_squareFreeCore_repeatedPart_primitive (f : ZPoly) (hf : f ≠ 0) : have d := f.primitiveSquareFreeDecomposition; (d.squareFreeCore * d.repeatedPart).Primitive

For nonzero input, the product of the square-free part and repeated part is primitive.

theorem Hex.ZPoly.primitiveSquareFreeDecomposition_squareFreeCore_eq_one_of_degree_zero (f : ZPoly) (hcore_ne : f.primitiveSquareFreeDecomposition.squareFreeCore ≠ 0) (hdegree : DensePoly.natDegree f.primitiveSquareFreeDecomposition.squareFreeCore = 0) : f.primitiveSquareFreeDecomposition.squareFreeCore = 1

A nonzero degree-zero square-free part from the primitive square-free decomposition is 1.

theorem Hex.ZPoly.primitiveSquareFreeDecomposition_repeatedPart_eq_one_of_squareFreeCore_degree_zero (f : ZPoly) (hcore_ne : f.primitiveSquareFreeDecomposition.squareFreeCore ≠ 0) (hdegree : DensePoly.natDegree f.primitiveSquareFreeDecomposition.squareFreeCore = 0) : f.primitiveSquareFreeDecomposition.repeatedPart = 1

Companion to primitiveSquareFreeDecomposition_squareFreeCore_eq_one_of_degree_zero: when the recorded square-free part has degree zero (and is nonzero), the recorded repeatedPart collapses to 1. The derivative-zero branch settles the goal by the literal repeatedPart := 1 field, while the derivative-nonzero branch is ruled out via the gcd-derivative degree arithmetic (derivative.size ≤ ratPrimitive.size - 1 combined with the quotient being a rational unit).

theorem Hex.ZPoly.leadingCoeff_squareFreeCore_nonneg (f : ZPoly) : 0 ≤ DensePoly.leadingCoeff f.primitiveSquareFreeDecomposition.squareFreeCore

The square-free part produced by primitive square-free decomposition has nonnegative leading coefficient.

theorem Hex.ZPoly.leadingCoeff_repeatedPart_nonneg (f : ZPoly) : 0 ≤ DensePoly.leadingCoeff f.primitiveSquareFreeDecomposition.repeatedPart

The repeated part produced by primitive square-free decomposition has nonnegative leading coefficient.

theorem Hex.ZPoly.primitiveSquareFreeDecomposition_squareFreeCore_repeatedPart_leadingCoeff_pos (f : ZPoly) (hf : f ≠ 0) : have d := f.primitiveSquareFreeDecomposition; 0 < DensePoly.leadingCoeff (d.squareFreeCore * d.repeatedPart)

For nonzero input, the product of the square-free part and repeated part has positive leading coefficient.

theorem Hex.ZPoly.primitiveSquareFreeDecomposition_reassembly_signed (f : ZPoly) (hf : f ≠ 0) : have d := f.primitiveSquareFreeDecomposition; ∃ (ε : Int), (ε = 1 ∨ ε = -1) ∧ DensePoly.scale ε (d.squareFreeCore * d.repeatedPart) = f.primitivePart

For nonzero input, the product of the square-free part and repeated part reassembles the primitive part up to sign.

theorem Hex.ZPoly.squareFreeCore_eq (f : ZPoly) : f.squareFreeCore = f.primitiveSquareFreeDecomposition.squareFreeCore

The squareFreeCore projection is the decomposition's square-free part. A definitional correspondence for consumers that cannot unfold the unexposed def.

theorem Hex.ZPoly.squareFreeCore_ne_zero (f : ZPoly) (hf : f ≠ 0) : f.squareFreeCore ≠ 0

The square-free part of a nonzero polynomial is nonzero: in the signed reassembly it is a factor of the (nonzero) primitive part.

theorem Hex.ZPoly.squareFreeCore_primitive (f : ZPoly) (hf : f ≠ 0) : f.squareFreeCore.Primitive

The square-free core of a nonzero polynomial is primitive.

theorem Hex.ZPoly.leadingCoeff_squareFreeCore_pos (f : ZPoly) (hf : f ≠ 0) : 0 < DensePoly.leadingCoeff f.squareFreeCore

The square-free core of a nonzero polynomial has positive leading coefficient.

theorem Hex.ZPoly.squareFreeRat_squareFreeCore (f : ZPoly) (hf : f ≠ 0) : f.squareFreeCore.SquareFreeRat

The square-free core of a nonzero polynomial is square-free over Rat[x]: combine the executable core square-freeness with core nonzeroness.

theorem Hex.ZPoly.toRatPoly_repeatedPart_dvd_derivative (f : ZPoly) : f.primitiveSquareFreeDecomposition.repeatedPart.toRatPoly ∣ f.primitivePart.toRatPoly.derivative

The rational cast of the repeated part divides the derivative of the rational cast of the primitive part. The repeated part is a rational associate of gcd(primitive, primitive'), which divides primitive'; this is the divisibility the square-free-part root transfer consumes.

theorem Hex.ZPoly.coprimeModP_of_bezout (f g s t : ZPoly) (p : Nat) (hbez : (s * f + t * g).congr 1 p) : f.coprimeModP g p

A Bezout congruence witness proves that two integer polynomials are coprime modulo p.

theorem Hex.ZPoly.dvd_of_toRatPoly_dvd_of_primitive {r f : ZPoly} (hr : r.Primitive) (hdvd : r.toRatPoly ∣ f.toRatPoly) : r ∣ f

Gauss descent: if a primitive integer polynomial r divides f over the rationals (ℚ[x]), then it divides f over the integers (ℤ[x]). The rational cofactor is cleared to a primitive integer polynomial via ratPolyPrimitivePart, and rational_associate_primitive_unit forces the leftover rational scalar to be ±1, so the integer product recovers f's primitive part exactly.

theorem Hex.ZPoly.primitiveSquareFreeDecomposition_repeatedPart_eq_one_of_squareFreeRat (core : ZPoly) (hne : core ≠ 0) (hsq : core.primitivePart.SquareFreeRat) : core.primitiveSquareFreeDecomposition.repeatedPart = 1

On a nonzero input whose primitive part is square-free over ℚ, the repeated part of the primitive square-free decomposition is 1.

theorem Hex.ZPoly.primitiveSquareFreeDecomposition_squareFreeCore_eq_of_squareFreeRat (core : ZPoly) (hne : core ≠ 0) (hsq : core.primitivePart.SquareFreeRat) : core.primitiveSquareFreeDecomposition.squareFreeCore = core.primitivePart.normalizePrimitiveSign

On a nonzero input whose primitive part is square-free over ℚ, the square-free part of the primitive square-free decomposition is exactly the sign-normalized primitive part. Together with primitiveSquareFreeDecomposition_repeatedPart_eq_one_of_squareFreeRat, this is the trivial decomposition that the modular square-free fast path returns.