of_mul_intCast — Mathlib

English

If x · m is irrational for some integer m, then x is irrational.

Русский

Если x · m иррационально для некоторого целого m, то x иррационально.

LaTeX

$$$$\forall x \in \mathbb{R}, \operatorname{Irrational}(x \cdot m) \Rightarrow \operatorname{Irrational}(x) \text{ for all } m \in \mathbb{Z}.$$$$

Lean4

theorem of_mul_intCast (m : ℤ) (h : Irrational (x * m)) : Irrational x :=
  of_mul_ratCast m <| by rwa [cast_intCast]

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