goldenConj_irrational

Mathlib.Data.Real.GoldenRatio

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

← MathLib Explorer

English

The conjugate ψ of φ is irrational.

Русский

Сопряжённое φ иррационально.

LaTeX

$$$\psi \notin \mathbb{Q}$$$

Lean4

/-- The conjugate of the golden ratio is irrational. -/
theorem goldenConj_irrational : Irrational ψ :=
  by
  have := Nat.Prime.irrational_sqrt (show Nat.Prime 5 by norm_num)
  have := this.ratCast_sub 1
  convert this.ratCast_mul (show (0.5 : ℚ) ≠ 0 by norm_num)
  norm_num
  field_simp

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

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

Разделы

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

Аффилиация

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