natCast_mul

Mathlib.RingTheory.Real.Irrational

URI: https://scilib.ai/kg/mathlib#Irrational.natCast_mul

English

If x is irrational, then m · x is irrational for nonzero 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 natCast_mul (h : Irrational x) {m : ℕ} (hm : m ≠ 0) : Irrational (m * x) :=
  h.intCast_mul <| Int.natCast_ne_zero.2 hm

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru