ofDigits_modEq

Mathlib.Data.Nat.Digits.Lemmas

URI: https://scilib.ai/kg/mathlib#Nat.ofDigits_modEq

English

For b,b',k and L, if b ≡ b' [MOD k], then ofDigits b L ≡ ofDigits b' L [MOD k].

Русский

Для b, b', k и L, если b ≡ b' [MOD k], то ofDigits b L ≡ ofDigits b' L [MOD k].

LaTeX

$$$ ofDigits\ b\ L \equiv ofDigits\ b'\ L [\text{MOD } k] \quad \text{при } b \equiv b' [\text{MOD } k]\,.$$$

Lean4

theorem ofDigits_modEq (b k : ℕ) (L : List ℕ) : ofDigits b L ≡ ofDigits (b % k) L [MOD k] :=
  ofDigits_modEq' b (b % k) k (b.mod_modEq k).symm L

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru