IsZeckendorfRep_nil

Mathlib.Data.Nat.Fib.Zeckendorf

URI: https://scilib.ai/kg/mathlib#List.IsZeckendorfRep_nil

English

The empty list [] is a Zeckendorf representation.

Русский

Пустой список [] является репрезентацией Зекендорфа.

LaTeX

$$$$ \operatorname{IsZeckendorfRep}(\ []) .$$$$

Lean4

@[simp]
theorem IsZeckendorfRep_nil : IsZeckendorfRep [] := by simp [IsZeckendorfRep]

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

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

Разделы

Аффилиация

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