fib_succ_sub_goldenRatio_mul_fib — Mathlib

English

Nat.fib(n+1) − φ · Nat.fib(n) = ψ^n.

Русский

Nat.fib(n+1) − φ · Nat.fib(n) = ψ^n.

LaTeX

$$$ \mathrm{Nat.fib}(n+1) - \phi \cdot \mathrm{Nat.fib}(n) = \psi^n $$$

Lean4

/-- Relationship between the Fibonacci Sequence, Golden Ratio and its conjugate's exponents -/
theorem fib_succ_sub_goldenRatio_mul_fib (n : ℕ) : Nat.fib (n + 1) - φ * Nat.fib n = ψ ^ n :=
  by
  repeat rw [coe_fib_eq]
  rw [mul_div, div_sub_div_same, mul_sub, ← pow_succ']
  ring_nf
  have nz : √5 ≠ 0 := by norm_num
  rw [← (mul_inv_cancel₀ nz).symm, one_mul]

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