irrational_neg_iff

Mathlib.RingTheory.Real.Irrational

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

English

For every real x, -x is irrational if and only if x is irrational.

Русский

Пусть x ∈ ℝ. Тогда иррациональность (-x) эквивалентна иррациональности x.

LaTeX

$$$\forall x \in \mathbb{R}, \operatorname{Irrational}(-x) \iff \operatorname{Irrational}(x)$$$

Lean4

@[simp]
theorem irrational_neg_iff : Irrational (-x) ↔ Irrational x :=
  ⟨of_neg, Irrational.neg⟩

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

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

Разделы

Аффилиация

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