instInv

Mathlib.Data.Real.Basic

URI: https://scilib.ai/kg/mathlib#Real.instInv

English

There is a total inverse operation on ℝ, denoted inv', giving multiplicative inverses.

Русский

Существуют обратные элементы в ℝ, обозначаемые inv', задающие обратные элементы для умножения.

LaTeX

$$$$\text{there exists } inv': \mathbb{R} \to \mathbb{R} \text{ with } x \cdot inv'(x) = 1 \text{ for } x \neq 0.$$$$

Lean4

noncomputable instance : Inv ℝ :=
  ⟨inv'⟩

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

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

Разделы

Аффилиация

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