structure Hex.Matrix.Lists.Scaled : Type

Integers representing a rational list with one positive denominator.

• denom : Nat
• nums : List Int

def Hex.Matrix.Lists.instReprScaled.repr : Scaled → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Hex.Matrix.Lists.instReprScaled : Repr Scaled

Equations

• Hex.Matrix.Lists.instReprScaled = { reprPrec := Hex.Matrix.Lists.instReprScaled.repr }

@[instance_reducible]

instance Hex.Matrix.Lists.instInhabitedScaled : Inhabited Scaled

Equations

• Hex.Matrix.Lists.instInhabitedScaled = { default := Hex.Matrix.Lists.instInhabitedScaled.default }

def Hex.Matrix.Lists.instDecidableEqScaled.decEq (x✝ x✝¹ : Scaled) : Decidable (x✝ = x✝¹)

Equations

• Hex.Matrix.Lists.instDecidableEqScaled.decEq { denom := a, nums := a_1 } { denom := b, nums := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Hex.Matrix.Lists.instDecidableEqScaled : DecidableEq Scaled

Equations

• Hex.Matrix.Lists.instDecidableEqScaled = Hex.Matrix.Lists.instDecidableEqScaled.decEq

structure Hex.Matrix.Lists.ScaledRows : Type

Integers representing a rational matrix with one positive denominator.

• denom : Nat
• nums : List (List Int)

def Hex.Matrix.Lists.instReprScaledRows.repr : ScaledRows → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Hex.Matrix.Lists.instReprScaledRows : Repr ScaledRows

Equations

• Hex.Matrix.Lists.instReprScaledRows = { reprPrec := Hex.Matrix.Lists.instReprScaledRows.repr }

@[instance_reducible]

instance Hex.Matrix.Lists.instInhabitedScaledRows : Inhabited ScaledRows

Equations

• Hex.Matrix.Lists.instInhabitedScaledRows = { default := Hex.Matrix.Lists.instInhabitedScaledRows.default }

def Hex.Matrix.Lists.instDecidableEqScaledRows.decEq (x✝ x✝¹ : ScaledRows) : Decidable (x✝ = x✝¹)

Equations

• Hex.Matrix.Lists.instDecidableEqScaledRows.decEq { denom := a, nums := a_1 } { denom := b, nums := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Hex.Matrix.Lists.instDecidableEqScaledRows : DecidableEq ScaledRows

Equations

• Hex.Matrix.Lists.instDecidableEqScaledRows = Hex.Matrix.Lists.instDecidableEqScaledRows.decEq

def Hex.Matrix.Lists.scaleRow (d : Nat) : List Rat → List Int → Bool

Cross products identify the original rational entries without rational arithmetic in the certificate checker.

Equations

• Hex.Matrix.Lists.scaleRow d [] [] = true
• Hex.Matrix.Lists.scaleRow d (q :: qs) (z :: zs) = (decide (q.num.mul (Int.ofNat d) = z.mul (Int.ofNat q.den)) && Hex.Matrix.Lists.scaleRow d qs zs)
• Hex.Matrix.Lists.scaleRow d x✝¹ x✝ = false

def Hex.Matrix.Lists.scaleRows (d : Nat) : List (List Rat) → List (List Int) → Bool

Check exact row lengths and entry agreement with a common denominator.

Equations

• Hex.Matrix.Lists.scaleRows d [] [] = true
• Hex.Matrix.Lists.scaleRows d (q :: qs) (z :: zs) = (Hex.Matrix.Lists.scaleRow d q z && Hex.Matrix.Lists.scaleRows d qs zs)
• Hex.Matrix.Lists.scaleRows d x✝¹ x✝ = false

def Hex.Matrix.Lists.Scaled.encode (xs : List Rat) : Scaled

Choose a common denominator once, in the compiled producer.

Equations

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

def Hex.Matrix.Lists.ScaledRows.encode (xs : List (List Rat)) : ScaledRows

Choose one common denominator for the entire matrix.

Equations

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

def Hex.Matrix.Lists.Scaled.add (a b : Scaled) : Scaled

Common denominators are cleared once per polynomial operation.

Equations

• a.add b = { denom := a.denom.mul b.denom, nums := Hex.Matrix.Lists.add (Hex.Matrix.Lists.scale (Int.ofNat b.denom) a.nums) (Hex.Matrix.Lists.scale (Int.ofNat a.denom) b.nums) }

def Hex.Matrix.Lists.Scaled.mul (a b : Scaled) : Scaled

Multiplication without rational normalization.

Equations

• a.mul b = { denom := a.denom.mul b.denom, nums := Hex.Matrix.Lists.mul a.nums b.nums }

def Hex.Matrix.Lists.Scaled.neg (a : Scaled) : Scaled

Negation with the denominator retained.

Equations

• a.neg = { denom := a.denom, nums := Hex.Matrix.Lists.scale (-1) a.nums }

def Hex.Matrix.Lists.Scaled.sub (a b : Scaled) : Scaled

Subtraction with cleared denominators.

Equations

• a.sub b = a.add b.neg

def Hex.Matrix.Lists.Scaled.pow (a : Scaled) : Nat → Scaled

Structural powers of a coefficient block.

Equations

• a.pow 0 = { denom := 1, nums := [1] }
• a.pow n.succ = (a.pow n).mul a