inv_goldenRatio

Mathlib.Data.Real.GoldenRatio

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

English

The reciprocal of the golden ratio equals minus its conjugate: φ^{-1} = -ψ.

Русский

Обратное к золотому сечению равно противоположности его сопряжённого: φ^{-1} = -ψ.

LaTeX

$$$\phi^{-1} = -\psi$$$

Lean4

/-- The inverse of the golden ratio is the opposite of its conjugate. -/
theorem inv_goldenRatio : φ⁻¹ = -ψ := by grind

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

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

Разделы

Аффилиация

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