ofDigits_singleton

Mathlib.Data.Nat.Digits.Defs

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

English

The value of a one-digit list is the digit itself (cast into the base).

Русский

Значение списка из одного элемента равно самой цифре (включая соответствующее приведение к основанию).

LaTeX

$$$\\operatorname{ofDigits}(b,[n]) = n$$$

Lean4

@[simp]
theorem ofDigits_singleton {b n : ℕ} : ofDigits b [n] = n := by simp [ofDigits]

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

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

Разделы

Аффилиация

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