coe_fib_eq

Mathlib.Data.Real.GoldenRatio

URI: https://scilib.ai/kg/mathlib#Real.coe_fib_eq

← MathLib Explorer

English

For all n, (Nat.fib n) viewed as a real equals (φ^n - ψ^n)/√5.

Русский

Для всех n вещественно отображаемое Nat.fib n равно (φ^n - ψ^n)/√5.

LaTeX

$$$ (\mathrm{Nat.fib} \, n : \mathbb{R}) = (\phi^n - \psi^n)/\sqrt{5} $$$

Lean4

/-- **Binet's formula** as a dependent equality. -/
theorem coe_fib_eq : ∀ n, (Nat.fib n : ℝ) = (φ ^ n - ψ ^ n) / √5 := by rw [← funext_iff, Real.coe_fib_eq']

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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