irrational_ratCast_mul_iff — Mathlib

English

Let q be a nonzero rational number and x a real number. Then q·x is irrational if and only if q ≠ 0 and x is irrational.

Русский

Пусть q ∈ ℚ, q ≠ 0, и x ∈ ℝ. Тогда qx иррационально тогда и только тогда, когда q ≠ 0 и x иррационально.

LaTeX

$$$\forall q \in \mathbb{Q}, \forall x \in \mathbb{R}, \operatorname{Irrational}(q \cdot x) \iff (q \neq 0 \land \operatorname{Irrational}(x))$$$

Lean4

@[simp]
theorem irrational_ratCast_mul_iff : Irrational (q * x) ↔ q ≠ 0 ∧ Irrational x :=
  ⟨fun h => ⟨Rat.cast_ne_zero.1 <| left_ne_zero_of_mul h.ne_zero, h.of_ratCast_mul q⟩, fun h => h.2.ratCast_mul h.1⟩

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