of_intCast_mul — Mathlib

English

If x is irrational and m is a natural number, then x − m is irrational.

Русский

Если x иррационально и m натуральное число, то x − m иррационально.

LaTeX

$$$$\forall x \in \mathbb{R}, \operatorname{Irrational}(x) \Rightarrow \forall m \in \mathbb{N}, \operatorname{Irrational}(x - m).$$$$

Lean4

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

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