invOf_mul_cancel_right

Mathlib.Algebra.Group.Invertible.Defs

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

English

In a monoid, (a b)^{-1} * b = a^{-1} and a * b * (a b)^{-1} = a.

Русский

В моноиде: (a b)^{-1} b = a^{-1} и a b (a b)^{-1} = a.

LaTeX

$$$ (a b)^{-1} b = a^{-1} \quad\text{and}\quad a b (a b)^{-1} = a$$$

Lean4

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

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

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

Разделы

Аффилиация

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