irrational — Mathlib

English

A Liouville number with exponent p > 1 is irrational.

Русский

Число Лиувилля с показателем p > 1 иррационально.

LaTeX

$$$$ \forall p \in \mathbb{R},\; \forall x \in \mathbb{R},\; LiouvilleWith(p,x) \land (1

Lean4

/-- A number satisfying the Liouville condition with exponent `p > 1` is an irrational number. -/
protected theorem irrational (h : LiouvilleWith p x) (hp : 1 < p) : Irrational x :=
  by
  rintro ⟨r, rfl⟩
  rcases eq_or_ne r 0 with (rfl | h0)
  · refine h.ne_cast_int hp 0 ?_; rw [Rat.cast_zero, Int.cast_zero]
  · refine (h.mul_rat (inv_ne_zero h0)).ne_cast_int hp 1 ?_
    rw [Rat.cast_inv, mul_inv_cancel₀]
    exacts [Int.cast_one.symm, Rat.cast_ne_zero.mpr h0]

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