class Hex.TSeries.UnitOps (R : Type u) : Type u

An executable partial inverse operation on a coefficient ring.

• inv? : R → Option R

  Return a multiplicative inverse when one is available.

class Hex.TSeries.LawfulUnitOps (R : Type u) [Lean.Grind.CommRing R] [UnitOps R] : Prop

Soundness and completeness of executable unit detection.

• inv?_eq (a u : R) : UnitOps.inv? a = some u → a * u = 1

  A returned inverse is a right inverse.

• inv?_isSome (a : R) : (∃ (u : R), a * u = 1) → (UnitOps.inv? a).isSome = true

  Every element admitting a right inverse is detected.

class Hex.TSeries.NatInverses (R : Type u) [Lean.Grind.CommRing R] (m : Nat) : Type u

Inverses of the natural numbers 1 through m in R.

• invNat : Nat → R

  A total lookup whose values are constrained on 1, ..., m.

• invNat_eq (k : Nat) : 1 ≤ k → k ≤ m → ↑k * invNat m k = 1

  The lookup inverts every required natural number.

@[instance_reducible]

def Hex.TSeries.NatInverses.mono {R : Type u} [Lean.Grind.CommRing R] {m m' : Nat} [NatInverses R m] (h : m' ≤ m) : NatInverses R m'

Restrict a family of natural inverses to a smaller precision. This is a definition rather than an instance to avoid instance-search loops.

Equations

• Hex.TSeries.NatInverses.mono h = { invNat := Hex.TSeries.NatInverses.invNat m, invNat_eq := ⋯ }

theorem Hex.TSeries.NatInverses.invNat_unique {R : Type u} [Lean.Grind.CommRing R] {m : Nat} (a b : NatInverses R m) (k : Nat) (hk : 1 ≤ k) (hkm : k ≤ m) : invNat m k = invNat m k

Any two lawful choices of the inverse of a required natural agree.

@[instance_reducible, instance 1100]

instance Hex.TSeries.instNatInversesOfNatNat {R : Type u_1} [Lean.Grind.CommRing R] : NatInverses R 0

No natural inverses are required at bound zero.

Equations

• Hex.TSeries.instNatInversesOfNatNat = { invNat := fun (x : Nat) => 0, invNat_eq := ⋯ }

@[instance_reducible, instance 1200]

instance Hex.TSeries.instNatInversesHSubNatOfNat {R : Type u_1} [Lean.Grind.CommRing R] (k : Nat) : NatInverses R (0 - k)

A subtraction from zero still requests no inverses. Keeping this syntactic instance is necessary across module boundaries, where instance matching need not unfold Nat.sub before comparing the index.

Equations

• Hex.TSeries.instNatInversesHSubNatOfNat k = { invNat := fun (x : Nat) => 0, invNat_eq := ⋯ }

@[instance_reducible, instance 1200]

instance Hex.TSeries.instNatInversesHSubNat {R : Type u_1} [Lean.Grind.CommRing R] (k : Nat) : NatInverses R (k - k)

A self-difference still requests no inverses. This makes the precision-one spelling NatInverses R (1 - 1) resolve without relying on kernel reduction of subtraction during typeclass search.

Equations

• Hex.TSeries.instNatInversesHSubNat k = { invNat := fun (x : Nat) => 0, invNat_eq := ⋯ }

@[instance_reducible, instance 1200]

instance Hex.TSeries.instNatInversesHSubNatOfNat_1 {R : Type u_1} [Lean.Grind.CommRing R] : NatInverses R (2 - 1)

The precision-two algorithm spelling requests NatInverses R (2 - 1). Keep that syntactic form available across module boundaries rather than relying on typeclass search to reduce the subtraction to one.

Equations

• Hex.TSeries.instNatInversesHSubNatOfNat_1 = { invNat := fun (x : Nat) => 1, invNat_eq := ⋯ }

@[instance_reducible, instance 1100]

instance Hex.TSeries.instNatInversesOfNatNat_1 {R : Type u_1} [Lean.Grind.CommRing R] : NatInverses R 1

At bound one, the only required inverse is 1.

Equations

• Hex.TSeries.instNatInversesOfNatNat_1 = { invNat := fun (x : Nat) => 1, invNat_eq := ⋯ }

@[instance_reducible]

instance Hex.TSeries.instUnitOpsRat : UnitOps Rat

Rational numbers have an executable inverse exactly away from zero.

Equations

• Hex.TSeries.instUnitOpsRat = { inv? := fun (a : Rat) => if a = 0 then none else some a⁻¹ }

instance Hex.TSeries.instLawfulUnitOpsRat : LawfulUnitOps Rat

Rational unit detection is sound and complete.

@[instance_reducible]

instance Hex.TSeries.instUnitOpsInt : UnitOps Int

The only integer units are 1 and -1.

Equations

• Hex.TSeries.instUnitOpsInt = { inv? := fun (a : Int) => if a = 1 then some 1 else if a = -1 then some (-1) else none }

instance Hex.TSeries.instLawfulUnitOpsInt : LawfulUnitOps Int

Integer unit detection is sound and complete.

@[instance_reducible, instance 900]

instance Hex.TSeries.instNatInversesRat (m : Nat) : NatInverses Rat m

Rational numbers contain inverses of every positive natural number.

Equations

• Hex.TSeries.instNatInversesRat m = { invNat := fun (k : Nat) => if k = 0 then 0 else (↑k)⁻¹, invNat_eq := ⋯ }