ne_one

Mathlib.RingTheory.Real.Irrational

URI: https://scilib.ai/kg/mathlib#Irrational.ne_one

English

If x ∈ ℝ is irrational, then x ≠ 1.

Русский

Пусть x ∈ ℝ иррационально. Тогда x ≠ 1.

LaTeX

$$$$\forall x \in \mathbb{R}, \operatorname{Irrational}(x) \rightarrow x \neq 1$$$$

Lean4

theorem ne_one (h : Irrational x) : x ≠ 1 := by simpa only [Nat.cast_one] using h.ne_nat 1

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

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

Разделы

Аффилиация

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