sum_zeckendorf_fib — Mathlib

English

For every n, the sum of Fibonacci numbers corresponding to the Zeckendorf representation of n equals n.

Русский

Для каждого n сумма чисел Фибоначчи, соответствующая репрезентации Зекендорфа n, равна n.

LaTeX

$$$$ \sum_{a \in \operatorname{zeckendorf}(n)} \operatorname{fib}(a) = n. $$$$

Lean4

@[simp]
theorem sum_zeckendorf_fib (n : ℕ) : (n.zeckendorf.map fib).sum = n := by
  induction n using zeckendorf.induct <;> simp_all [fib_greatestFib_le]

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