ofDigits_zmodeq' — Mathlib

English

For integers b, k and list L, the digits base b with modulo k satisfy ofDigits(b,L) ≡ ofDigits(b mod k, L) (mod k).

Русский

Для целых b, k и списка L выполняется ofDigits(b,L) ≡ ofDigits(b mod k, L) (mod k).

LaTeX

$$$\operatorname{ofDigits}(b,L) \bmod k = \operatorname{ofDigits}(b \,\%\, k, L) \bmod k$$$

Lean4

theorem ofDigits_zmodeq' (b b' : ℤ) (k : ℕ) (h : b ≡ b' [ZMOD k]) (L : List ℕ) :
    ofDigits b L ≡ ofDigits b' L [ZMOD k] := by
  induction L with
  | nil => rfl
  | cons d L ih =>
    dsimp [ofDigits]
    dsimp [Int.ModEq] at *
    conv_lhs => rw [Int.add_emod, Int.mul_emod, h, ih]
    conv_rhs => rw [Int.add_emod, Int.mul_emod]

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