inv_goldenConj

Mathlib.Data.Real.GoldenRatio

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

/-- The opposite of the golden ratio is the inverse of its conjugate. -/
theorem inv_goldenConj : ψ⁻¹ = -φ :=
  by
  rw [inv_eq_iff_eq_inv, ← neg_inv, ← neg_eq_iff_eq_neg]
  exact inv_goldenRatio.symm

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

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

Разделы

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

Аффилиация

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