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}.

Русский

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

LaTeX

$$$(a b)^{-1} b = a^{-1}$$$

Lean4

@[simp]
theorem invOf_mul_cancel_right' [Monoid α] (a b : α) {_ : Invertible b} : a * ⅟b * b = a := by simp [mul_assoc]

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

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

Разделы

Аффилиация

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