zeckendorf_succ — Mathlib

English

zeckendorf(n+1) = greatestFib(n+1) :: zeckendorf(n+1 - fib(greatestFib(n+1))).

Русский

zeckendorf(n+1) = greatestFib(n+1) :: zeckendorf(n+1 - fib(greatestFib(n+1))).

LaTeX

$$$$ \operatorname{zeckendorf}(n+1) = \operatorname{greatestFib}(n+1) :: \operatorname{zeckendorf}(n+1 - \operatorname{fib}(\operatorname{greatestFib}(n+1))). $$$$

Lean4

@[simp]
theorem zeckendorf_succ (n : ℕ) :
    zeckendorf (n + 1) = greatestFib (n + 1) :: zeckendorf (n + 1 - fib (greatestFib (n + 1))) :=
  zeckendorf.eq_2 ..

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