of_mul_ratCast

Mathlib.RingTheory.Real.Irrational

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

English

If x · q is irrational for some q ∈ ℚ, then x is irrational.

Русский

Если x · q иррационально для некоторых рациональных q, то x иррационально.

LaTeX

$$$$\forall (q \in \mathbb{Q}), \operatorname{Irrational}(x q) \Rightarrow \operatorname{Irrational}(x).$$$$

Lean4

theorem of_mul_ratCast (h : Irrational (x * q)) : Irrational x :=
  h.mul_cases.resolve_right q.not_irrational

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

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

Разделы

Аффилиация

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