goldenConj_neg

Mathlib.Data.Real.GoldenRatio

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

English

ψ < 0

Русский

ψ < 0

LaTeX

$$$ \psi < 0 $$$

Lean4

theorem goldenConj_neg : ψ < 0 := by linarith [one_sub_goldenConj, one_lt_goldenRatio]

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

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

Разделы

Аффилиация

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