intCast_div — Mathlib

English

If x is irrational, then for every nonzero integer m, m/x is irrational.

Русский

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

LaTeX

$$$\operatorname{Irrational}(x) \Rightarrow \forall m \in \mathbb{Z}, m \neq 0 \Rightarrow \operatorname{Irrational}(m/x)$$$

Lean4

theorem intCast_div (h : Irrational x) {m : ℤ} (hm : m ≠ 0) : Irrational (m / x) :=
  h.inv.intCast_mul hm

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