intCast_mul

Mathlib.RingTheory.Real.Irrational

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

← MathLib Explorer

English

If x is irrational and m ≠ 0, then m · x is irrational.

Русский

Если x иррационально и m ≠ 0, то m · x иррационально.

LaTeX

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

Lean4

theorem intCast_mul (h : Irrational x) {m : ℤ} (hm : m ≠ 0) : Irrational (m * x) :=
  mul_comm x m ▸ h.mul_intCast hm

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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