ofDigits_zmodeq — Mathlib

English

Given natural bases b and b', and c ∈ ℤ with b' ≡ c (mod b), for any n, n ≡ ofDigits c (digits b' n) (mod b).

Русский

Пусть b и b' — натуральные основания, c ∈ ℤ such that b' ≡ c (ZMOD b). Тогда для любого n выполняется n ≡ ofDigits c (digits b' n) (mod b).

LaTeX

$$$n \equiv \operatorname{ofDigits}(c, \operatorname{digits}(b',n)) \,[ZMOD\ b]$$$

Lean4

theorem ofDigits_zmodeq (b : ℤ) (k : ℕ) (L : List ℕ) : ofDigits b L ≡ ofDigits (b % k) L [ZMOD k] :=
  ofDigits_zmodeq' b (b % k) k (b.mod_modEq ↑k).symm L

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