class Hex.ExactDivLaws (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.

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

  Right multiplication followed by division by a nonzero factor cancels.

theorem Hex.ExactDivLaws.mul_right_cancel {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] {a b c : R} (hc : c ≠ 0) (h : a * c = b * c) : a = b

Exact division implies right cancellation by a nonzero factor.

theorem Hex.ExactDivLaws.mul_ne_zero {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] {a b : R} (ha : a ≠ 0) (hb : b ≠ 0) : a * b ≠ 0

Exact division and commutative-ring laws rule out nonzero products vanishing.

theorem Hex.one_ne_zero_of_nonzero {S : Type u} [Lean.Grind.CommRing S] {a : S} (ha : a ≠ 0) : 1 ≠ 0

A nonzero element witnesses that a lightweight ring is nontrivial.

theorem Hex.negOne_ne_zero_of_one {S : Type u} [Lean.Grind.CommRing S] (h1 : 1 ≠ 0) : 0 - 1 ≠ 0

The additive inverse of one is nonzero in a nontrivial lightweight ring.

def Hex.exactDiv {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.

Equations

• Hex.exactDiv a b = if b = 0 then 0 else a / b

@[simp]

theorem Hex.exactDiv_zero_right {R : Type u} [Zero R] [DecidableEq R] [Div R] (a : R) : exactDiv a 0 = 0

Exact division by zero takes the stable junk branch.

theorem Hex.exactDiv_eq_div_of_ne {R : Type u} [Zero R] [DecidableEq R] [Div R] (a : R) {b : R} (hb : b ≠ 0) : exactDiv a b = a / b

A nonzero exact quotient is the underlying quotient operation.

@[simp]

theorem Hex.exactDiv_mul_right {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] [Div R] [ExactDivLaws R] (a : R) {b : R} (hb : b ≠ 0) : exactDiv (a * b) b = a

The wrapper cancels a nonzero exact right factor under ExactDivLaws.

instance Hex.instExactDivLawsInt : ExactDivLaws Int

Integer Euclidean division is exact on nonzero right multiples.

class Hex.DomainLaws (R : Type u) [Zero R] [One R] [Mul R] : Prop

A nontrivial ring without zero divisors. Proof-only: a certificate checker that needs no quotient operation states its soundness over this class rather than over ExactDivLaws, so that a consumer re-checking a witness never has to supply a division.

• one_ne_zero : 1 ≠ 0

  The ring is nontrivial.

• no_zero_div (a b : R) : a * b = 0 → a = 0 ∨ b = 0

  A vanishing product has a vanishing factor.

instance Hex.instDomainLawsInt : DomainLaws Int

The integers form a domain.

instance Hex.instDomainLawsField {K : Type u} [Lean.Grind.Field K] : DomainLaws K

Every Lean.Grind.Field is a domain.

theorem Hex.DomainLaws.of_exactDivLaws {R : Type u} [Lean.Grind.CommRing R] [Div R] [ExactDivLaws R] (h1 : 1 ≠ 0) : DomainLaws R

An exact quotient on a nontrivial ring rules out zero divisors. Stated as a theorem rather than an instance because ExactDivLaws alone does not imply nontriviality: the trivial ring satisfies it vacuously.

instance Hex.instExactDivLawsField {K : Type u} [Lean.Grind.Field K] : ExactDivLaws K

Every Lean.Grind.Field supplies the exact-division law.