irrational — Mathlib

English

Any transcendental real number over ℚ is irrational.

Русский

Любое трансцендентальное вещественное число над ℚ иррационально.

LaTeX

$$$\text{Transcendental}_{\mathbb{Q}}(r) \Rightarrow \mathrm{Irrational}(r)$$$

Lean4

/-- A transcendental real number is irrational. -/
theorem irrational {r : ℝ} (tr : Transcendental ℚ r) : Irrational r :=
  by
  rintro ⟨a, rfl⟩
  exact tr (isAlgebraic_algebraMap a)

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