goldenRatio_irrational

Mathlib.Data.Real.GoldenRatio

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

← MathLib Explorer

English

The golden ratio φ is irrational.

Русский

Золотое отношение иррационально.

LaTeX

$$$\phi \notin \mathbb{Q}$$$

Lean4

/-- The golden ratio is irrational. -/
theorem goldenRatio_irrational : Irrational φ :=
  by
  have := Nat.Prime.irrational_sqrt (show Nat.Prime 5 by norm_num)
  have := this.ratCast_add 1
  convert this.ratCast_mul (show (0.5 : ℚ) ≠ 0 by norm_num)
  norm_num
  field_simp

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

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

Разделы

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

Аффилиация

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