inv

Mathlib.RingTheory.Real.Irrational

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

English

If x is irrational, then x⁻¹ is irrational.

Русский

Если x иррационально, то x⁻¹ иррационально.

LaTeX

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

Lean4

protected theorem inv (h : Irrational x) : Irrational x⁻¹ :=
  of_inv <| by rwa [inv_inv]

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

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

Разделы

Аффилиация

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