neg

Mathlib.RingTheory.Real.Irrational

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

English

If -x is irrational, then x is irrational.

Русский

Если -x иррационально, то x иррационален.

LaTeX

$$$\operatorname{Irrational}(-x) \Rightarrow \operatorname{Irrational}(x)$$$

Lean4

protected theorem neg (h : Irrational x) : Irrational (-x) :=
  of_neg <| by rwa [neg_neg]

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

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

Разделы

Аффилиация

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