of_inv

Mathlib.RingTheory.Real.Irrational

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

English

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

Русский

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

LaTeX

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

Lean4

theorem of_inv (h : Irrational x⁻¹) : Irrational x := fun ⟨q, hq⟩ => h <| hq ▸ ⟨q⁻¹, q.cast_inv⟩

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

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

Разделы

Аффилиация

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