mul_intCast — Mathlib

English

If x is irrational, then m − x is irrational for every natural m.

Русский

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

LaTeX

$$$$\forall x \in \mathbb{R}, \operatorname{Irrational}(x) \Rightarrow \forall m \in \mathbb{N}, \operatorname{Irrational}(m - x).$$$$

Lean4

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

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