def Hex.NumberTower.isZero {T : NumberTower} (a : T.Elem) : Bool

Boolean zero test on fixed mixed-radix coordinates.

Equations

• Hex.NumberTower.isZero a = (Hex.NumberTower.coeffs a).all fun (q : Rat) => decide (q = 0)

def Hex.NumberTower.zero (T : NumberTower) : T.Elem

Additive identity.

Equations

• T.zero = T.ofCoeffs #[]

@[instance_reducible]

instance Hex.NumberTower.instZeroElem {T : NumberTower} : Zero T.Elem

Equations

• Hex.NumberTower.instZeroElem = { zero := T.zero }

theorem Hex.NumberTower.zero_eq_ofRat (T : NumberTower) : 0 = T.ofRat 0

The coordinate zero is the rational embedding of zero.

@[simp]

theorem Hex.NumberTower.coeffs_zero (T : NumberTower) : coeffs 0 = Array.replicate T.dim 0

Zero exposes the all-zero fixed-width coordinate array.

theorem Hex.NumberTower.isZero_iff_eq_zero {T : NumberTower} (a : T.Elem) : isZero a = true ↔ a = 0

The Boolean coordinate test recognizes exactly the tower zero.

def Hex.NumberTower.one (T : NumberTower) : T.Elem

Multiplicative identity.

Equations

• T.one = T.ofCoeffs #[1]

@[instance_reducible]

instance Hex.NumberTower.instOneElem {T : NumberTower} : One T.Elem

Equations

• Hex.NumberTower.instOneElem = { one := T.one }

theorem Hex.NumberTower.one_eq_ofRat (T : NumberTower) : 1 = T.ofRat 1

The coordinate one is the rational embedding of one.

def Hex.NumberTower.add {T : NumberTower} (a b : T.Elem) : T.Elem

Coordinatewise addition.

Equations

• Hex.NumberTower.add a b = T.ofCoeffs (Hex.NumberTower.Arithmetic.addCoords T.dim (Hex.NumberTower.coeffs a) (Hex.NumberTower.coeffs b))

@[instance_reducible]

instance Hex.NumberTower.instAddElem {T : NumberTower} : Add T.Elem

Equations

• Hex.NumberTower.instAddElem = { add := Hex.NumberTower.add }

@[simp]

theorem Hex.NumberTower.coeffs_add {T : NumberTower} (a b : T.Elem) : coeffs (a + b) = Arithmetic.addCoords T.dim (coeffs a) (coeffs b)

Addition exposes its fixed-width coordinate result.

def Hex.NumberTower.sub {T : NumberTower} (a b : T.Elem) : T.Elem

Coordinatewise subtraction.

Equations

• Hex.NumberTower.sub a b = T.ofCoeffs (Hex.NumberTower.Arithmetic.subCoords T.dim (Hex.NumberTower.coeffs a) (Hex.NumberTower.coeffs b))

@[instance_reducible]

instance Hex.NumberTower.instSubElem {T : NumberTower} : Sub T.Elem

Equations

• Hex.NumberTower.instSubElem = { sub := Hex.NumberTower.sub }

@[simp]

theorem Hex.NumberTower.coeffs_sub {T : NumberTower} (a b : T.Elem) : coeffs (a - b) = Arithmetic.subCoords T.dim (coeffs a) (coeffs b)

Subtraction exposes its fixed-width coordinate result.

def Hex.NumberTower.neg {T : NumberTower} (a : T.Elem) : T.Elem

Coordinatewise additive inverse.

Equations

• Hex.NumberTower.neg a = Hex.NumberTower.Internal.ofCoeffs T (Hex.NumberTower.Arithmetic.negCoords T.dim (Hex.NumberTower.coeffs a)) ⋯

@[instance_reducible]

instance Hex.NumberTower.instNegElem {T : NumberTower} : Neg T.Elem

Equations

• Hex.NumberTower.instNegElem = { neg := Hex.NumberTower.neg }

@[simp]

theorem Hex.NumberTower.coeffs_neg {T : NumberTower} (a : T.Elem) : coeffs (-a) = Arithmetic.negCoords T.dim (coeffs a)

Negation exposes its fixed-width coordinate result.

theorem Hex.NumberTower.sub_eq_add_neg {T : NumberTower} (a b : T.Elem) : a - b = a + -b

Coordinate subtraction is addition of the coordinatewise negation.

theorem Hex.NumberTower.add_neg_self {T : NumberTower} (a : T.Elem) : a + -a = 0

Coordinatewise negation is an additive inverse.

def Hex.NumberTower.mul {T : NumberTower} (a b : T.Elem) : T.Elem

Recursive convolution and monic reduction.

Equations

• Hex.NumberTower.mul a b = T.ofCoeffs (Hex.NumberTower.Arithmetic.mulCoords T.levels.toList (Hex.NumberTower.coeffs a) (Hex.NumberTower.coeffs b))

@[instance_reducible]

instance Hex.NumberTower.instMulElem {T : NumberTower} : Mul T.Elem

Equations

• Hex.NumberTower.instMulElem = { mul := Hex.NumberTower.mul }

@[simp]

theorem Hex.NumberTower.coeffs_mul {T : NumberTower} (a b : T.Elem) : coeffs (a * b) = Arithmetic.mulCoords T.levels.toList (coeffs a) (coeffs b)

Multiplication exposes its fixed-width recursively reduced coordinates.

def Hex.NumberTower.inv {T : NumberTower} (a : T.Elem) : T.Elem

Recursive extended-gcd inversion, totalized by 0⁻¹ = 0.

Equations

• Hex.NumberTower.inv a = T.ofCoeffs (Hex.NumberTower.Arithmetic.invCoords T.levels.toList (Hex.NumberTower.coeffs a))

@[instance_reducible]

instance Hex.NumberTower.instInvElem {T : NumberTower} : Inv T.Elem

Equations

• Hex.NumberTower.instInvElem = { inv := Hex.NumberTower.inv }

@[simp]

theorem Hex.NumberTower.coeffs_inv {T : NumberTower} (a : T.Elem) : coeffs a⁻¹ = Arithmetic.invCoords T.levels.toList (coeffs a)

Recursive inversion exposes its fixed-width extended-gcd coordinates.

def Hex.NumberTower.div {T : NumberTower} (a b : T.Elem) : T.Elem

Tower division.

Equations

• Hex.NumberTower.div a b = a * b⁻¹

@[instance_reducible]

instance Hex.NumberTower.instDivElem {T : NumberTower} : Div T.Elem

Equations

• Hex.NumberTower.instDivElem = { div := Hex.NumberTower.div }

def Hex.NumberTower.smul {T : NumberTower} (q : Rat) (a : T.Elem) : T.Elem

Rational scalar multiplication acts on every mixed-radix coordinate.

Equations

• Hex.NumberTower.smul q a = T.ofCoeffs (Array.map (fun (c : Rat) => q * c) (Hex.NumberTower.coeffs a))

@[instance_reducible]

instance Hex.NumberTower.instSMulRatElem {T : NumberTower} : SMul Rat T.Elem

Equations

• Hex.NumberTower.instSMulRatElem = { smul := Hex.NumberTower.smul }

def Hex.NumberTower.natPow {T : NumberTower} (a : T.Elem) : Nat → T.Elem

Natural powers by repeated tower multiplication.

Equations

• Hex.NumberTower.natPow a 0 = 1
• Hex.NumberTower.natPow a n.succ = Hex.NumberTower.natPow a n * a

@[instance_reducible]

instance Hex.NumberTower.instPowElemNat {T : NumberTower} : Pow T.Elem Nat

Equations

• Hex.NumberTower.instPowElemNat = { pow := Hex.NumberTower.natPow }

def Hex.NumberTower.intPow {T : NumberTower} (a : T.Elem) : Int → T.Elem

Integer powers from natural powers and inversion, with 0⁻¹ = 0.

Equations

• Hex.NumberTower.intPow a (Int.ofNat n) = Hex.NumberTower.natPow a n
• Hex.NumberTower.intPow a (Int.negSucc n) = (Hex.NumberTower.natPow a (n + 1))⁻¹

@[instance_reducible]

instance Hex.NumberTower.instPowElemInt {T : NumberTower} : Pow T.Elem Int

Equations

• Hex.NumberTower.instPowElemInt = { pow := Hex.NumberTower.intPow }

@[instance_reducible]

instance Hex.NumberTower.instNatCastElem {T : NumberTower} : NatCast T.Elem

Equations

• Hex.NumberTower.instNatCastElem = { natCast := fun (n : Nat) => T.ofRat ↑n }

@[instance_reducible]

instance Hex.NumberTower.instIntCastElem {T : NumberTower} : IntCast T.Elem

Equations

• Hex.NumberTower.instIntCastElem = { intCast := fun (n : Int) => T.ofRat ↑n }

@[instance_reducible, instance 90]

instance Hex.NumberTower.instOfNatElemHAddNatOfNat {T : NumberTower} (n : Nat) : OfNat T.Elem (n + 2)

Equations

• Hex.NumberTower.instOfNatElemHAddNatOfNat n = { ofNat := T.ofRat ↑(n + 2) }

@[simp]

theorem Hex.NumberTower.coeffs_smul {T : NumberTower} (q : Rat) (a : T.Elem) : coeffs (q • a) = Array.map (fun (c : Rat) => q * c) (coeffs a)

Rational scalar multiplication exposes coordinatewise multiplication.

@[reducible, inline]

abbrev Hex.NumberTower.Poly (T : NumberTower) : Type

Dense univariate polynomials over a fixed tower.

Equations

• T.Poly = Hex.DensePoly T.Elem