one_sub_goldenConj

Mathlib.Data.Real.GoldenRatio

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

English

One minus the conjugate equals the golden ratio: 1 − ψ = φ.

Русский

Единица минус сопряжённое равняется золотому сечению: 1 − ψ = φ.

LaTeX

$$$1 - \psi = \phi$$$

Lean4

theorem one_sub_goldenConj : 1 - φ = ψ := by linarith [goldenRatio_add_goldenConj]

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

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

Разделы

Аффилиация

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