transcendental_liouvilleNumber — Mathlib

English

For m ≥ 2, the Liouville number liouvilleNumber m.cast is transcendental over the integers.

Русский

Для m ≥ 2 число Лиувиля liouvilleNumber m.cast является трансцендентальным над целыми.

LaTeX

$$$ \forall m \in \mathbb N,\ 2 \le m \Rightarrow \operatorname{Transcendental}_{\mathbb Z}(\liouvilleNumber m.cast)$$$

Lean4

theorem transcendental_liouvilleNumber {m : ℕ} (hm : 2 ≤ m) : Transcendental ℤ (liouvilleNumber m) :=
  (liouville_liouvilleNumber hm).transcendental

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