Documentation

Projects.Util.Digits.Basic

source
theorem Nat.base_iff {b : ℕ} :
b.Base ↔ 2 ≤ b
source
theorem Nat.base_iff_decide {b : ℕ} :
b.Base ↔ Base.decide b = true
source
@[instance_reducible]
instance Nat.instDecidableBase {b : ℕ} :
Decidable b.Base
Equations
source
@[simp]
instance Nat.instBaseOfNat :
Base 2
source
@[simp]
instance Nat.instBaseOfNat_1 :
Base 10
source
@[simp]
theorem Nat.Base.two_le {b : ℕ} [hb : b.Base] :
2 ≤ b
source
@[simp]
theorem Nat.Base.one_lt {b : ℕ} [hb : b.Base] :
1 < b
source
@[simp]
theorem Nat.Base.one_le {b : ℕ} [hb : b.Base] :
1 ≤ b
source
@[simp]
theorem Nat.Base.pos {b : ℕ} [hb : b.Base] :
0 < b
source
@[simp]
theorem Nat.Base.ne_zero {b : ℕ} [hb : b.Base] :
b ≠ 0
source
theorem Nat.Base.div_lt {b : ℕ} [hb : b.Base] {n : ℕ} (h : b ≤ n) :
n / b < n
source
@[simp]
theorem Nat.Base.not_le_one {b : ℕ} [hb : b.Base] :
¬b ≤ 1
source
@[simp]
theorem Nat.Base.one_mod {b : ℕ} [hb : b.Base] :
1 % b = 1
source
@[simp]
theorem Nat.Base.one_div {b : ℕ} [hb : b.Base] :
1 / b = 0
source
theorem Nat.Base.sub_div_mul_sub_one_succ_lt {b : ℕ} [hb : b.Base] {n : ℕ} :
n - n / b * (b - 1) + 1 < n + b
source
@[simp]
theorem Nat.toDigList_zero {b : ℕ} [hb : b.Base] :
b.toDigList 0 = [0]
source
@[simp]
theorem Nat.toDigList_one {b : ℕ} [hb : b.Base] :
b.toDigList 1 = [1]
source
theorem Nat.lt_pow_digsNum {b : ℕ} [hb : b.Base] {n : ℕ} :
n < b ^ b.digsNum n
source
theorem Nat.lt_pow_of_digsNum_eq {b : ℕ} [hb : b.Base] {n k : ℕ} (h : b.digsNum n = k) :
n < b ^ k
source
@[simp]
theorem Nat.sum_toDigList'_zero {b : ℕ} :
(b.toDigList' 0).sum = 0
source
@[simp]
theorem Nat.sum_toDigList'_le {b n : ℕ} :
(b.toDigList' n).sum ≤ n
source
@[simp]
theorem Nat.sum_toDigList_le {b n : ℕ} :
(b.toDigList n).sum ≤ n
source
@[simp]
theorem Nat.digSum_le {b n : ℕ} :
b.digSum n ≤ n
source
@[simp]
theorem Nat.not_lt_sum_toDigList' {b n : ℕ} :
¬n < (b.toDigList' n).sum
source
@[simp]
theorem Nat.not_lt_sum_toDigList {b n : ℕ} :
¬n < (b.toDigList n).sum
source
@[simp]
theorem Nat.not_lt_digSum {b n : ℕ} :
¬n < b.digSum n
source
@[simp]
theorem Nat.toDigList_base_zero_succ {n : ℕ} :
toDigList 0 (n + 1) = []
source
@[simp]
theorem Nat.toDigList_base_one_succ {n : ℕ} :
toDigList 1 (n + 1) = []
source
@[simp]
theorem Nat.digSum_base_zero {n : ℕ} :
digSum 0 n = 0
source
@[simp]
theorem Nat.digSum_base_one {n : ℕ} :
digSum 1 n = 0
source
theorem Nat.toDigList'_of_lt_base {b n : ℕ} (hn : n ≠ 0) (h : n < b) :
b.toDigList' n = [n]
source
theorem Nat.toDigList_of_lt_base {b : ℕ} [hb : b.Base] {n : ℕ} (h : n < b) :
b.toDigList n = [n]
source
@[simp]
theorem Nat.digSum_zero {b : ℕ} :
b.digSum 0 = 0
source
@[simp]
theorem Nat.digSum_one {b : ℕ} [hb : b.Base] :
b.digSum 1 = 1
source
theorem Nat.digSum_of_lt_base {b n : ℕ} (h : n < b) :
b.digSum n = n
source
theorem Nat.digSum_lt_iff_base_le {b : ℕ} [hb : b.Base] {n : ℕ} :
b.digSum n < n ↔ b ≤ n
source
theorem Nat.digSum_of_base_le_one {b n : ℕ} (hb : b ≤ 1) :
b.digSum n = 0
source
@[simp]
theorem Nat.digSum_eq_self_iff {b : ℕ} [hb : b.Base] {n : ℕ} :
b.digSum n = n ↔ n = 0 ∨ n < b
source
theorem Nat.digSum_step {b : ℕ} [hb : b.Base] {n : ℕ} :
b.digSum n = n % b + b.digSum (n / b)
source
@[simp]
theorem Nat.digSum_base {b : ℕ} [hb : b.Base] :
b.digSum b = 1
source
theorem Nat.digSum_add_base_of_lt_base {b : ℕ} [hb : b.Base] {n : ℕ} (h : n < b) :
b.digSum (n + b) = n + 1
source
@[simp]
theorem Nat.digSum_eq_zero_iff {b n : ℕ} :
b.digSum n = 0 ↔ b ≤ 1 ∨ n = 0
source
@[simp]
theorem Nat.digSum_mul_base {b n : ℕ} :
b.digSum (n * b) = b.digSum n
source
@[simp]
theorem Nat.digSum_base_mul {b n : ℕ} :
b.digSum (b * n) = b.digSum n
source
@[simp]
theorem Nat.digSum_mul_base_pow {b n k : ℕ} :
b.digSum (n * b ^ k) = b.digSum n
source
@[simp]
theorem Nat.digSum_base_mul_pow {b n k : ℕ} :
b.digSum (b ^ k * n) = b.digSum n
source
theorem Nat.digSum_mul_base_add {b : ℕ} [hb : b.Base] {n k : ℕ} (hk : k < b) :
b.digSum (n * b + k) = b.digSum n + k
source
theorem Nat.digSum_base_add {b : ℕ} [hb : b.Base] {n : ℕ} (hk : n < b) :
b.digSum (b + n) = n + 1
source
theorem Nat.digSum_add_base {b : ℕ} [hb : b.Base] {n : ℕ} (hk : n < b) :
b.digSum (n + b) = n + 1
source
theorem Nat.ind_dig (b : ℕ) [hb : b.Base] {p : ℕ → Prop} (h₁ : ∀ c < b, p c) (h₂ : ∀ (k c : ℕ), k ≠ 0 → c < b → (∀ m < k * b + c, p m) → p (k * b + c)) (n : ℕ) :
p n
source
theorem Nat.digSum_mod_base_pred {b : ℕ} [hb : b.Base] {n : ℕ} :
b.digSum n % (b - 1) = n % (b - 1)
source
@[simp]
theorem Nat.ofDigList_singleton {b n : ℕ} :
b.ofDigList [n] = n
source
theorem Nat.toDigList'_mul_base_add {b : ℕ} [hb : b.Base] {k c : ℕ} (hk : k ≠ 0) (hc : c < b) :
b.toDigList' (k * b + c) = c :: b.toDigList' k
source
theorem Nat.toDigList_mul_base_add {b : ℕ} [hb : b.Base] {k c : ℕ} (hk : k ≠ 0) (hc : c < b) :
b.toDigList (k * b + c) = b.toDigList k ++ [c]
source
@[simp]
theorem Nat.Base.ne_one {b : ℕ} [hb : b.Base] :
b ≠ 1
source
@[simp]
theorem Nat.ofDigList_toDigList {b : ℕ} [hb : b.Base] {n : ℕ} :
b.ofDigList (b.toDigList n) = n
source
@[simp]
theorem Nat.toDigList'_zero {b : ℕ} [hb : b.Base] :
b.toDigList' 0 = []
source
@[simp]
theorem Nat.toDigList'_eq_nil_iff {b : ℕ} [hb : b.Base] {n : ℕ} :
b.toDigList' n = [] ↔ n = 0
source
@[simp]
theorem Nat.toDigList_ne_nil {b : ℕ} [hb : b.Base] {n : ℕ} :
b.toDigList n ≠ []
source
theorem Nat.digRev_of_lt_base {b : ℕ} [hb : b.Base] {n : ℕ} (h : n < b) :
b.digRev n = n
source
@[simp]
theorem Nat.ofDigList_nil {b : ℕ} :
b.ofDigList [] = 0
source
@[simp]
theorem Nat.ofDigList_snoc {b : ℕ} [hb : b.Base] {c : ℕ} {cs : List ℕ} :
b.ofDigList (cs ++ [c]) = b.ofDigList cs * b + c
source
@[simp]
theorem Nat.ofDigList_cons {b c : ℕ} {cs : List ℕ} :
b.ofDigList (c :: cs) = c * b ^ cs.length + b.ofDigList cs
source
theorem Nat.toDigList_mul_base {b : ℕ} [hb : b.Base] {k : ℕ} (hk : k ≠ 0) :
b.toDigList (k * b) = b.toDigList k ++ [0]
source
@[simp]
theorem Nat.digRev_mul_base {b : ℕ} [hb : b.Base] {k : ℕ} :
b.digRev (k * b) = b.digRev k
source
theorem Nat.digRev_mul_base_add {b : ℕ} [hb : b.Base] {k c : ℕ} (hk : k ≠ 0) (hc : c < b) :
b.digRev (k * b + c) = c * b ^ b.digsNum k + b.digRev k
source
theorem Nat.digsNum_eq_iff {b : ℕ} [hb : b.Base] {n k : ℕ} :
b.digsNum n = k ↔ n = 0 ∧ k = 1 ∨ k ≠ 0 ∧ b ^ (k - 1) ≤ n ∧ n < b ^ k
source
theorem Nat.digRev_eq_of_digsNum_eq_two {b : ℕ} [hb : b.Base] {n : ℕ} (h : b.digsNum n = 2) :
b.digRev n = n % b * b + n / b
source
@[simp]
theorem Nat.digsNum_zero {b : ℕ} [hb : b.Base] :
b.digsNum 0 = 1
source
theorem Nat.digsNum_of_lt_base {b : ℕ} [hb : b.Base] {n : ℕ} (hn : n < b) :
b.digsNum n = 1
source
theorem Nat.digsNum_base_mul_add {b : ℕ} [hb : b.Base] {k c : ℕ} (hk : k ≠ 0) (hc : c < b) :
b.digsNum (k * b + c) = b.digsNum k + 1
source
theorem Nat.digsNum_base_mul {b : ℕ} [hb : b.Base] {k : ℕ} (hk : k ≠ 0) :
b.digsNum (k * b) = b.digsNum k + 1
source
@[irreducible]
def Nat.digSumAlt₁ (b n : ℕ) :
ℕ
Equations
Instances For
    source
    @[csimp]
    theorem Nat.digSum_eq_digSumAlt₁ :
    digSum = digSumAlt₁