irrational_intCast_mul_iff — Mathlib

English

Let m be an integer and x a real number. Then m·x is irrational iff m ≠ 0 and x is irrational.

Русский

Пусть m ∈ ℤ и x ∈ ℝ. Тогда m·x иррационально тогда и только тогда, когда m ≠ 0 и x иррационально.

LaTeX

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

Lean4

@[simp]
theorem irrational_intCast_mul_iff : Irrational (m * x) ↔ m ≠ 0 ∧ Irrational x := by
  rw [← cast_intCast, irrational_ratCast_mul_iff, Int.cast_ne_zero]

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