def DigitalRoot.digRootList (b : ℕ) (xs : List ℕ) : ℕ

Equations

• DigitalRoot.digRootList b xs = DigitalRoot.digRoot b xs.sum

@[simp]

theorem DigitalRoot.digRootList_lt_base {b : ℕ} [hb : b.Base] {n : List ℕ} : digRootList b n < b

@[simp]

theorem DigitalRoot.digRootList_le_base {b : ℕ} {n : List ℕ} : digRootList b n ≤ b

@[simp]

theorem DigitalRoot.digRootList_nil {b : ℕ} : digRootList b [] = 0

@[simp]

theorem DigitalRoot.digRootList_cons {b : ℕ} [hb : b.Base] {x : ℕ} {xs : List ℕ} : digRootList b (x :: xs) = digRoot b (x + digRootList b xs)