goldenRatio

Mathlib.Data.Real.GoldenRatio

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

English

embedReal maps 1 to 1 in ℝ.

Русский

embedReal(1) = 1.

LaTeX

$$$\operatorname{embedReal}(M)(1) = 1$$$

Lean4

/-- The golden ratio `φ := (1 + √5)/2`. -/
abbrev goldenRatio : ℝ :=
  (1 + √5) / 2

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

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

Разделы

Аффилиация

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