mul_ratCast — Mathlib

English

If x is irrational and q ≠ 0, then q · x is irrational.

Русский

Если x иррационально и q ≠ 0, то q · x иррационально.

LaTeX

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

Lean4

theorem mul_ratCast (h : Irrational x) {q : ℚ} (hq : q ≠ 0) : Irrational (x * q) :=
  of_mul_ratCast q⁻¹ <| by rwa [mul_assoc, ← cast_mul, mul_inv_cancel₀ hq, cast_one, mul_one]

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