mul_natCast — Mathlib

English

If x is irrational, then m · x is irrational for any nonzero natural m.

Русский

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

LaTeX

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

Lean4

theorem mul_natCast (h : Irrational x) {m : ℕ} (hm : m ≠ 0) : Irrational (x * m) :=
  h.mul_intCast <| Int.natCast_ne_zero.2 hm

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