noncomputable def DigitalRoot.digRoot (b n : ℕ) : ℕ

Equations

• DigitalRoot.digRoot b n = Function.fix b.digSum n

def DigitalRoot.digRootAlt₁' (b n g : ℕ) : ℕ

Equations

• DigitalRoot.digRootAlt₁' b n 0 = n
• DigitalRoot.digRootAlt₁' b n g_2.succ = if n < b then n else DigitalRoot.digRootAlt₁' b (b.digSum n) g_2

def DigitalRoot.digRootAlt₁ (b n : ℕ) : ℕ

Equations

• DigitalRoot.digRootAlt₁ b n = DigitalRoot.digRootAlt₁' b n n

@[irreducible]

noncomputable def DigitalRoot.digRootAlt₂ (b n : ℕ) : ℕ

Equations

• DigitalRoot.digRootAlt₂ b n = if ¬b.Base then 0 else if n < b then n else DigitalRoot.digRootAlt₂ b (b.digSum n)

def DigitalRoot.digRootAlt₃ (b n : ℕ) : ℕ

Equations

• DigitalRoot.digRootAlt₃ b n = if b ≤ 1 ∨ n = 0 then 0 else if n % (b - 1) = 0 then b - 1 else n % (b - 1)