of_div_intCast

Mathlib.RingTheory.Real.Irrational

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

English

For any integer m, if x/m is irrational, then x is irrational.

Русский

Для любого целого m, если x/m иррационально, то x иррационален.

LaTeX

$$$\forall m \in \mathbb{Z}, \; \operatorname{Irrational}(x/m) \Rightarrow \operatorname{Irrational}(x)$$$

Lean4

theorem of_div_intCast (m : ℤ) (h : Irrational (x / m)) : Irrational x :=
  h.div_cases.resolve_right m.not_irrational

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

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

Разделы

Аффилиация

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