hex

1.4. Exact division🔗

Fraction-free algorithms need a coefficient-independent way to say that a division operation cancels a known nonzero factor. The law package isolates that assumption from the executable wrapper.

🔗type class
Hex.ExactDivLaws.{u} (R : Type u) [Zero R] [Mul R] [Div R] : Prop
Hex.ExactDivLaws.{u} (R : Type u) [Zero R]
  [Mul R] [Div R] : Prop

A quotient operation is exact when multiplication by every nonzero right factor can be undone by division by that factor.

Instance Constructor

Hex.ExactDivLaws.mk.{u}

Methods

mul_div_cancel_right : ∀ (a b : R), b ≠ 0 → a * b / b = a

Right multiplication followed by division by a nonzero factor cancels.

🔗def
Hex.exactDiv.{u} {R : Type u} [Zero R] [DecidableEq R] [Div R]
  (a b : R) : R
Hex.exactDiv.{u} {R : Type u} [Zero R]
  [DecidableEq R] [Div R] (a b : R) : R

Total exact quotient wrapper. The zero denominator is a documented junk input and returns zero.

The zero denominator has a deterministic value, while the nonzero branch is the carrier's ordinary division. Integers and lightweight fields provide the standard instances.

open Hex #guard exactDiv (21 : Int) 3 = 7 #guard exactDiv (21 : Int) 0 = 0