of_add_ratCast

Mathlib.RingTheory.Real.Irrational

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

English

If q+x is irrational, then x is irrational.

Русский

Если q+x иррационально, то x иррационально.

LaTeX

$$$$\operatorname{Irrational}(q+x) \rightarrow \operatorname{Irrational}(x)$$$$

Lean4

theorem of_add_ratCast : Irrational (x + q) → Irrational x :=
  add_comm (↑q) x ▸ of_ratCast_add q

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

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

Разделы

Аффилиация

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