inductive Hex.ZPoly.DivExact.Reject : Type

The first cheap obstruction found before integer-polynomial long division.

The constructors are ordered by the cost of the corresponding check.

• zeroDivisor : Reject

  Division by the zero polynomial is undefined.

• degree : Reject

  A nonzero divisor cannot have larger degree than a nonzero dividend.

• leadingCoeff : Reject

  The divisor's leading coefficient must divide the dividend's.

• content : Reject

  The divisor's coefficient content must divide the dividend's.

• evaluation : Reject

  Divisibility must survive evaluation at the fixed small point.

@[instance_reducible]

instance Hex.ZPoly.DivExact.instBEqReject : BEq Reject

Equations

• Hex.ZPoly.DivExact.instBEqReject = { beq := Hex.ZPoly.DivExact.instBEqReject.beq }

def Hex.ZPoly.DivExact.instBEqReject.beq : Reject → Reject → Bool

Equations

• Hex.ZPoly.DivExact.instBEqReject.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[instance_reducible]

instance Hex.ZPoly.DivExact.instDecidableEqReject : DecidableEq Reject

Equations

• Hex.ZPoly.DivExact.instDecidableEqReject x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Hex.ZPoly.DivExact.instReprReject : Repr Reject

Equations

• Hex.ZPoly.DivExact.instReprReject = { reprPrec := Hex.ZPoly.DivExact.instReprReject.repr }

def Hex.ZPoly.DivExact.instReprReject.repr : Reject → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def Hex.ZPoly.DivExact.evalPoint : Int

The fixed small evaluation point used by the final exact-division precheck.

Evaluation at one avoids coefficient growth while still testing a condition independent of the degree, leading-coefficient, and content checks.

Equations

• Hex.ZPoly.DivExact.evalPoint = 1

def Hex.ZPoly.DivExact.contentValue (f : ZPoly) : Int

Executable coefficient content used by exact-division rejection.

Equations

• Hex.ZPoly.DivExact.contentValue f = Int.ofNat (Hex.DensePoly.contentNatImpl f)

theorem Hex.ZPoly.DivExact.contentValue_eq (f : ZPoly) : contentValue f = f.content

The executable content value agrees with the public specification.

def Hex.ZPoly.DivExact.evalValue (f : ZPoly) : Int

Executable Horner evaluation at the fixed rejection point.

Equations

• Hex.ZPoly.DivExact.evalValue f = Hex.DensePoly.evalImpl f Hex.ZPoly.DivExact.evalPoint

theorem Hex.ZPoly.DivExact.evalValue_eq (f : ZPoly) : evalValue f = DensePoly.eval f evalPoint

The executable evaluation value agrees with public polynomial evaluation.

def Hex.ZPoly.DivExact.reject? (f g : ZPoly) : Option Reject

Return the first cheap reason that g cannot divide f, or none when dense exact division is still necessary.

The zero dividend is deliberately allowed past the degree check: every nonzero polynomial divides zero, with exact quotient zero.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.ZPoly.DivExact.reject?_eq_none_of_mul (q g : ZPoly) (hg : g ≠ 0) : reject? (q * g) g = none

Every exact multiple passes all cheap rejection tests.

def Hex.ZPoly.divExact? (f g : ZPoly) : Option ZPoly

The exact quotient f / g, or none when g = 0 or the executable integer-polynomial division does not reconstruct f exactly.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Hex.ZPoly.divExact?_zero_right (f : ZPoly) : f.divExact? 0 = none

Division by the zero polynomial is always rejected.

theorem Hex.ZPoly.divExact?_eq_none_of_reject {f g : ZPoly} {reason : DivExact.Reject} (h : DivExact.reject? f g = some reason) : f.divExact? g = none

A prefilter rejection returns before the dense-division branch.

theorem Hex.ZPoly.divExact?_product {f g q : ZPoly} (h : f.divExact? g = some q) : q * g = f

A successful exact division carries the checked multiplication witness.

theorem Hex.ZPoly.divMod_eq_mul_of_ne_zero (f g q : ZPoly) (hg : g ≠ 0) (hmul : q * g = f) : DensePoly.divMod f g = (q, 0)

Long division returns the witnessed quotient for every exact multiple by a nonzero integer polynomial.

theorem Hex.ZPoly.divExact?_eq {f g q : ZPoly} (hg : g ≠ 0) : f.divExact? g = some q ↔ f = q * g

Exact division succeeds exactly on a supplied multiplication witness when the divisor is nonzero.

theorem Hex.ZPoly.divExact?_isSome_of_dvd {f g : ZPoly} (hg : g ≠ 0) : g ∣ f → (f.divExact? g).isSome = true

Every nonzero divisor is found by the executable exact-division check.