irrational_div_ratCast_iff — Mathlib

English

Let q be a rational number and x a real number. Then x/q is irrational iff q ≠ 0 and x is irrational.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem irrational_div_ratCast_iff : Irrational (x / q) ↔ q ≠ 0 ∧ Irrational x := by
  rw [div_eq_mul_inv, ← cast_inv, irrational_mul_ratCast_iff, Ne, inv_eq_zero]

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