not_irrational_ofNat

Mathlib.RingTheory.Real.Irrational

URI: https://scilib.ai/kg/mathlib#not_irrational_ofNat

English

For all n with AtLeastTwo, Irrational(ofNat(n)) is false.

Русский

Для всех n с условием AtLeastTwo, Irrational(ofNat(n)) ложно.

LaTeX

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

Lean4

@[simp]
theorem not_irrational_ofNat (n : ℕ) [n.AtLeastTwo] : ¬Irrational ofNat(n) :=
  n.not_irrational

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

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

Разделы

Аффилиация

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