digits_getLast — Mathlib

English

Let b > 1. For any natural m and any indices p, q, the p-th from the end digit of the base-b representation of m equals the q-th from the end digit of the base-b representation of m div b.

Русский

Пусть b > 1. Для любого натурального m и любых индексов p, q p-ая с конца цифра числа m в основании b равна q-я с конца цифра числа m div b в основании b.

LaTeX

$$$ (digits\ b\ m).getLast(p) = (digits\ b\ (m / b)).getLast(q) $$$

Lean4

theorem digits_getLast {b : ℕ} (m : ℕ) (h : 1 < b) (p q) : (digits b m).getLast p = (digits b (m / b)).getLast q :=
  by
  by_cases hm : m = 0
  · simp [hm]
  simp only [digits_eq_cons_digits_div h hm]
  rw [List.getLast_cons]

Похожие утверждения