ofDigits_digits_append_digits — Mathlib

English

If p ≤ q then ofDigits p L ≤ ofDigits q L for any list L of digits.

Русский

Если p ≤ q, то ofDigits p L ≤ ofDigits q L для любого списка цифр L.

LaTeX

$$$ \forall L:\mathrm{List}\ \mathbb{N},\ p\le q\Rightarrow \mathrm{ofDigits}(p,L) \le \mathrm{ofDigits}(q,L) $$$

Lean4

theorem ofDigits_digits_append_digits {b m n : ℕ} :
    ofDigits b (digits b n ++ digits b m) = n + b ^ (digits b n).length * m := by
  rw [ofDigits_append, ofDigits_digits, ofDigits_digits]

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