invOf_eq_group_inv

Mathlib.Algebra.Group.Invertible.Defs

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

English

In a group, the inverse of an element a is its two-sided inverse a^{-1}.

Русский

В группе обратная к элементу a — это его двусторонняя обратная a^{-1}.

LaTeX

$$$\\forall a\\in G:\\, \\ a \\cdot a^{-1} = a^{-1} \\cdot a = 1$$$

Lean4

@[simp]
theorem invOf_eq_group_inv [Group α] (a : α) [Invertible a] : ⅟a = a⁻¹ :=
  invOf_eq_right_inv (mul_inv_cancel a)

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

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

Разделы

Аффилиация

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