invOf_mul_cancel_left

Mathlib.Algebra.Group.Invertible.Defs

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

English

In a monoid, inv a * (a b) = b; hence a*(b) has inverse structure.

Русский

В моноиде inv(a) * (a b) = b; следовательно, существует структура обратного к a и b.

LaTeX

$$$\operatorname{inv}(a) (a b) = b$$$

Lean4

theorem invOf_mul_cancel_left [Monoid α] (a b : α) [Invertible a] : ⅟a * (a * b) = b :=
  invOf_mul_cancel_left' _ _

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

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

Разделы

Аффилиация

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