digits_zero_succ

Mathlib.Data.Nat.Digits.Defs

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

English

A refinement stating digits for base 0 with n ≠ 0 is a singleton list.

Русский

Уточнение: для основания 0, если n ≠ 0, то digits(0,n) = [n].

LaTeX

$$$\text{digits}(0,n) = [n] \text{ if } n \neq 0$$$

Lean4

@[simp]
theorem digits_zero_succ (n : ℕ) : digits 0 n.succ = [n + 1] :=
  rfl

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

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

Разделы

Аффилиация

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