of_ratCast_add

Mathlib.RingTheory.Real.Irrational

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

English

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

Русский

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

LaTeX

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

Lean4

theorem of_ratCast_add (h : Irrational (q + x)) : Irrational x :=
  h.add_cases.resolve_left q.not_irrational

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

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

Разделы

Аффилиация

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