div_ratCast — Mathlib

English

If x is irrational, then x/q is irrational for any nonzero rational q.

Русский

Если x иррационально, то x/q иррационально для любого ненулевого рационального q.

LaTeX

$$$\forall q \in \mathbb{Q}, q \neq 0 \Rightarrow \operatorname{Irr}(x/q)$$$

Lean4

theorem div_ratCast (h : Irrational x) {q : ℚ} (hq : q ≠ 0) : Irrational (x / q) :=
  by
  rw [div_eq_mul_inv, ← cast_inv]
  exact h.mul_ratCast (inv_ne_zero hq)

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