structure Hex.SquareFreeInput : Type

A square-free part presented to classical factorization. The executable layer stores the polynomial; the Mathlib correctness layer supplies and retains the normalization invariants.

• poly : ZPoly

  The square-free part to be factored.

def Hex.instDecidableEqSquareFreeInput.decEq (x✝ x✝¹ : SquareFreeInput) : Decidable (x✝ = x✝¹)

Equations

• Hex.instDecidableEqSquareFreeInput.decEq { poly := a } { poly := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Hex.instDecidableEqSquareFreeInput : DecidableEq SquareFreeInput

Equations

• Hex.instDecidableEqSquareFreeInput = Hex.instDecidableEqSquareFreeInput.decEq

def Hex.SquareFreeInput.ofNormalized (normalized : FactorNormalizationData) : SquareFreeInput

Package the primitive square-free part produced by the common normalization pass.

Equations

• Hex.SquareFreeInput.ofNormalized normalized = { poly := normalized.squareFreeCore }