class Nat.Base (b : ℕ) : Prop

• h : 2 ≤ b

def Nat.Base.decide (b : ℕ) : Bool

Equations

• Nat.Base.decide b = decide (2 ≤ b)

@[irreducible]

def Nat.toDigList' (b n : ℕ) : List ℕ

Equations

• b.toDigList' n = if b ≤ 1 then [] else if n = 0 then [] else n % b :: b.toDigList' (n / b)

def Nat.toDigList (b n : ℕ) : List ℕ

Equations

• b.toDigList n = if b ≤ 1 then [] else if n = 0 then [0] else (b.toDigList' n).reverse

def Nat.ofDigList (b : ℕ) (ds : List ℕ) : ℕ

Equations

• b.ofDigList ds = List.foldl (fun (n d : ℕ) => n * b + d) 0 ds

def Nat.digSum (b n : ℕ) : ℕ

Equations

• b.digSum n = (b.toDigList n).sum

def Nat.digRev (b n : ℕ) : ℕ

Equations

• b.digRev n = b.ofDigList (b.toDigList n).reverse

def Nat.digsNum (b n : ℕ) : ℕ

Equations

• b.digsNum n = (b.toDigList n).length