ofDigits_append_zero

Mathlib.Data.Nat.Digits.Defs

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

← MathLib Explorer

English

Appending a trailing zero to a digit list does not change its value.

Русский

Добавление в конец списка цифр нуля не меняет его значения.

LaTeX

$$$\\operatorname{ofDigits}(b, l ++ [0]) = \\operatorname{ofDigits}(b, l).$$$

Lean4

@[simp]
theorem ofDigits_append_zero {b : ℕ} (l : List ℕ) : ofDigits b (l ++ [0]) = ofDigits b l := by
  rw [ofDigits_append, ofDigits_singleton, mul_zero, add_zero]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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