mul_invOf_cancel_right'

Mathlib.Algebra.Group.Invertible.Defs

URI: https://scilib.ai/kg/mathlib#mul_invOf_cancel_right'

English

For any a, b in a monoid with b invertible, a * b * b^{-1} = a.

Русский

Для любых a, b в моноиде с обратимым b, a b b^{-1} = a.

LaTeX

$$$a \cdot b \cdot b^{-1} = a$$$

Lean4

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

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

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

Разделы

Аффилиация

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