ne_ofNat

Mathlib.RingTheory.Real.Irrational

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

English

For every n ≥ 2, ofNat(n) is not irrational.

Русский

Для каждого n ≥ 2 число ofNat(n) не иррационально.

LaTeX

$$$$\forall n \in \mathbb{N}, n \ge 2 \rightarrow \neg \operatorname{Irrational}(\operatorname{ofNat}(n))$$$$

Lean4

@[simp]
theorem ne_ofNat (h : Irrational x) (n : ℕ) [n.AtLeastTwo] : x ≠ ofNat(n) :=
  h.ne_nat n

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

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

Разделы

Аффилиация

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