of_mul_self

Mathlib.RingTheory.Real.Irrational

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

English

If x^2 is irrational, then x is irrational.

Русский

Если x^2 иррационально, то x иррационален.

LaTeX

$$$\operatorname{Irrational}(x\cdot x) \Rightarrow \operatorname{Irrational}(x)$$$

Lean4

theorem of_mul_self (h : Irrational (x * x)) : Irrational x :=
  h.mul_cases.elim id id

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

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

Разделы

Аффилиация

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