ofDigits_modEq' — Mathlib

English

If b ≡ b' (mod k), then for any L, ofDigits(b,L) ≡ ofDigits(b',L) (mod k).

Русский

Если b ≡ b' (mod k), то для любого L выполняется ofDigits(b,L) ≡ ofDigits(b',L) (mod k).

LaTeX

$$$ ofDigits\, b\, L \\equiv ofDigits\, b'\\, L \\ [\\mathrm{MOD}\\ k] $ если $ b \\equiv b' \\ [\\mathrm{MOD}\\ k] $.$$

Lean4

theorem ofDigits_modEq' (b b' : ℕ) (k : ℕ) (h : b ≡ b' [MOD k]) (L : List ℕ) : ofDigits b L ≡ ofDigits b' L [MOD k] :=
  by
  induction L with
  | nil => rfl
  | cons d L ih =>
    dsimp [ofDigits]
    dsimp [Nat.ModEq] at *
    conv_lhs => rw [Nat.add_mod, Nat.mul_mod, h, ih]
    conv_rhs => rw [Nat.add_mod, Nat.mul_mod]

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