invOf_units

Mathlib.Algebra.Group.Invertible.Basic

URI: https://scilib.ai/kg/mathlib#invOf_units

English

For a unit u, the inverse in the ambient monoid equals the image of its inverse in the unit group.

Русский

Для единицы u обратное в моноиде равно образу её обратного в группе единиц.

LaTeX

$$$ \operatorname{invOf} (u) = (u^{-1})^{\uparrow}$$$

Lean4

@[simp]
theorem invOf_units [Monoid α] (u : αˣ) [Invertible (u : α)] : ⅟(u : α) = ↑u⁻¹ :=
  invOf_eq_right_inv u.mul_inv

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

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

Разделы

Аффилиация

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