goldenRatio_pow_sub_goldenRatio_pow

Mathlib.Data.Real.GoldenRatio

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

English

Let φ denote the golden ratio. For every natural number n, φ^(n+2) − φ^(n+1) = φ^n.

Русский

Пусть φ обозначает золотое сечение. Для каждого натурального числа n выполняется φ^(n+2) − φ^(n+1) = φ^n.

LaTeX

$$$ \phi^{n+2} - \phi^{n+1} = \phi^n $$$

Lean4

theorem goldenRatio_pow_sub_goldenRatio_pow (n : ℕ) : φ ^ (n + 2) - φ ^ (n + 1) = φ ^ n := by grind

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

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

Разделы

Аффилиация

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