ofDigits_mod — Mathlib

English

The relation modulo k for digits holds after replacing base by b with b ≡ b' (mod k).

Русский

Относительно модуля k число цифр сохраняется при замене основания на эквивалентное по модулю k.

LaTeX

$$$ \operatorname{ofDigits}(b,L) \equiv \operatorname{ofDigits}(b',L) [ZMOD\ k] \text{ при } b \equiv b' [ZMOD\ k]. $$$

Lean4

theorem ofDigits_mod (b k : ℕ) (L : List ℕ) : ofDigits b L % k = ofDigits (b % k) L % k :=
  ofDigits_modEq b k L

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