div_intCast — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem div_intCast (h : Irrational x) {m : ℤ} (hm : m ≠ 0) : Irrational (x / m) :=
  by
  rw [← cast_intCast]
  refine h.div_ratCast ?_
  rwa [Int.cast_ne_zero]

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