ofDigits_zmod

Mathlib.Data.Nat.Digits.Lemmas

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

English

For b ∈ ℤ, k ∈ ℕ, and L, we have ofDigits b L mod k equals ofDigits (b mod k) L mod k.

Русский

Для b ∈ ℤ, k ∈ ℕ и L выполняется ofDigits b L mod k = ofDigits (b mod k) L mod k.

LaTeX

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

Lean4

theorem ofDigits_zmod (b : ℤ) (k : ℕ) (L : List ℕ) : ofDigits b L % k = ofDigits (b % k) L % k :=
  ofDigits_zmodeq b k L

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

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

Разделы

Аффилиация

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