one_sub_goldenRatio

Mathlib.Data.Real.GoldenRatio

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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