Documentation

Projects.DigitalRoot.Basic

source
theorem DigitalRoot.digRoot_spec {b n : ℕ} :
digRoot b n = b.digSum^[n] n ∧ b.digSum (digRoot b n) = digRoot b n
source
theorem DigitalRoot.digRoot_eq_iterate {b n : ℕ} :
digRoot b n = b.digSum^[n] n
source
@[simp]
theorem DigitalRoot.digSum_digRoot {b n : ℕ} :
b.digSum (digRoot b n) = digRoot b n
source
@[simp]
theorem DigitalRoot.digRoot_digSum {b n : ℕ} :
digRoot b (b.digSum n) = digRoot b n
source
@[simp]
theorem DigitalRoot.digRootAlt₁'_gas_zero {b n : ℕ} :
digRootAlt₁' b n 0 = n
source
@[simp]
theorem DigitalRoot.digRootAlt₁'_zero {b g : ℕ} :
digRootAlt₁' b 0 g = 0
source
theorem DigitalRoot.digRootAlt₁'_base_le_one {b n g : ℕ} (h₁ : b ≤ 1) (h₂ : g ≠ 0) :
digRootAlt₁' b n g = 0
source
theorem DigitalRoot.digRootAlt₁'_of_lt_base {b n g : ℕ} (h : n < b) :
digRootAlt₁' b n g = n
source
@[simp]
theorem DigitalRoot.digRootAlt₁'_gas_succ {b n g : ℕ} :
digRootAlt₁' b n (g + 1) = digRootAlt₁' b (b.digSum n) g
source
theorem DigitalRoot.digRoot_eq_digRootAlt₁ :
digRoot = digRootAlt₁
source
theorem DigitalRoot.digRoot_of_lt_base {b n : ℕ} (h : n < b) :
digRoot b n = n
source
theorem DigitalRoot.digRoot_step {b n : ℕ} :
digRoot b n = digRoot b (b.digSum n)
source
@[simp]
theorem DigitalRoot.digRoot_zero {b : ℕ} :
digRoot b 0 = 0
source
theorem DigitalRoot.digRoot_of_base_le_one {b n : ℕ} (hb : b ≤ 1) :
digRoot b n = 0
source
theorem DigitalRoot.digRoot_eq_digRootAlt₂ :
digRoot = digRootAlt₂
source
@[simp]
theorem DigitalRoot.digRoot_base_zero {n : ℕ} :
digRoot 0 n = 0
source
@[simp]
theorem DigitalRoot.digRoot_base_one {n : ℕ} :
digRoot 1 n = 0
source
theorem DigitalRoot.digRoot_lt_base_of {b n : ℕ} (hb : b ≠ 0) :
digRoot b n < b
source
@[simp]
theorem DigitalRoot.digRoot_lt_Nat.base_iff {b n : ℕ} :
digRoot b n < b ↔ b ≠ 0
source
@[simp]
theorem DigitalRoot.digRoot_digRoot {b n : ℕ} :
digRoot b (digRoot b n) = digRoot b n
source
@[simp]
theorem DigitalRoot.digRoot_base {b : ℕ} [hb : b.Base] :
digRoot b b = 1
source
theorem DigitalRoot.digRoot_eq_digSum_of {b : ℕ} [hb : b.Base] {n : ℕ} (h : n + 1 < b * 2) :
digRoot b n = b.digSum n
source
@[simp]
theorem DigitalRoot.digRoot_base_sub_one {b : ℕ} :
digRoot b (b - 1) = b - 1
source
@[simp]
theorem DigitalRoot.digRoot_base_two {n : ℕ} :
digRoot 2 n = if n = 0 then 0 else 1
source
@[simp]
theorem DigitalRoot.digRoot_one {b : ℕ} [hb : b.Base] :
digRoot b 1 = 1
source
@[simp]
theorem DigitalRoot.digRoot_mul_base {b n : ℕ} :
digRoot b (n * b) = digRoot b n
source
@[simp]
theorem DigitalRoot.digRoot_base_mul {b n : ℕ} :
digRoot b (b * n) = digRoot b n
source
@[simp]
theorem DigitalRoot.digRoot_mul_base_pow {b n k : ℕ} :
digRoot b (n * b ^ k) = digRoot b n
source
@[simp]
theorem DigitalRoot.digRoot_base_pow_mul {b n k : ℕ} :
digRoot b (b ^ k * n) = digRoot b n
source
@[simp]
theorem DigitalRoot.digRoot_mod_base_pred {b : ℕ} [hb : b.Base] {n : ℕ} :
digRoot b n % (b - 1) = n % (b - 1)
source
@[simp]
theorem DigitalRoot.digRoot_eq_zero_iff {b n : ℕ} :
digRoot b n = 0 ↔ b ≤ 1 ∨ n = 0
source
@[simp]
theorem DigitalRoot.digRoot_base_succ_le {b n : ℕ} :
digRoot (b + 1) n ≤ b
source
@[simp]
theorem DigitalRoot.digRoot_le_base_pred {b n : ℕ} :
digRoot b n ≤ b - 1
source
theorem DigitalRoot.digRoot_add_base {b n : ℕ} :
digRoot b (n + b) = digRoot b (n + 1)
source
theorem DigitalRoot.digRoot_add_base_pred {b n : ℕ} (hn : n ≠ 0) :
digRoot b (n + (b - 1)) = digRoot b n
source
@[csimp]
theorem DigitalRoot.digRoot_eq_digRootAlt₃ :
digRoot = digRootAlt₃
source
theorem DigitalRoot.digRoot_add {b : ℕ} [hb : b.Base] {n m : ℕ} :
digRoot b (n + m) = digRoot b (digRoot b n + digRoot b m)
source
@[simp]
theorem DigitalRoot.digRoot_add_digRoot_succ_lt_base_mul_two_iff {b n m : ℕ} :
digRoot b n + digRoot b m + 1 < b * 2 ↔ b ≠ 0
source
theorem DigitalRoot.digRoot_add' {b : ℕ} [hb : b.Base] {n m : ℕ} :
digRoot b (n + m) = b.digSum (digRoot b n + digRoot b m)
source
@[simp]
theorem DigitalRoot.digRoot_mul_base_add {b : ℕ} [hb : b.Base] {n k : ℕ} :
digRoot b (n * b + k) = digRoot b (n + k)
source
@[simp]
theorem DigitalRoot.digRoot_base_pred_add {b n : ℕ} (h : n ≠ 0) :
digRoot b (b - 1 + n) = digRoot b n
source
@[simp]
theorem DigitalRoot.digRoot_digRoot_add_left {b : ℕ} [hb : b.Base] {n m : ℕ} :
digRoot b (n + digRoot b m) = digRoot b (n + m)
source
@[simp]
theorem DigitalRoot.digRoot_digRoot_add_right {b : ℕ} [hb : b.Base] {n m : ℕ} :
digRoot b (digRoot b n + m) = digRoot b (n + m)
source
@[simp]
theorem DigitalRoot.digRoot_eq_self_iff {b : ℕ} [hb : b.Base] {n : ℕ} :
digRoot b n = n ↔ n < b
source
@[simp]
theorem DigitalRoot.digRoot_le_base {b n : ℕ} :
digRoot b n ≤ b