ofDigits_mod_eq_head!

Mathlib.Data.Nat.Digits.Lemmas

URI: https://scilib.ai/kg/mathlib#Nat.ofDigits_mod_eq_head!

English

For base b and list L, the remainder of ofDigits(b,L) modulo b equals the head of L modulo b.

Русский

При основании b и списке L остаток от деления ofDigits(b,L) на b равен остатку списка L на b.

LaTeX

$$$\operatorname{ofDigits}(b,L) \bmod b = L.head! \bmod b$$$

Lean4

theorem ofDigits_mod_eq_head! (b : ℕ) (l : List ℕ) : ofDigits b l % b = l.head! % b := by
  induction l <;> simp [Nat.ofDigits]

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

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

Разделы

Аффилиация

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