irrational_natCast_mul_iff — Mathlib

English

Let n be a natural number and x a real number. Then n·x is irrational iff n ≠ 0 and x is irrational.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem irrational_natCast_mul_iff : Irrational (n * x) ↔ n ≠ 0 ∧ Irrational x := by
  rw [← cast_natCast, irrational_ratCast_mul_iff, Nat.cast_ne_zero]

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