mul_invOf_cancel_left'

Mathlib.Algebra.Group.Invertible.Defs

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

English

In a monoid, a * (inv a * b) = b.

Русский

В моноиде: a * (inv a * b) = b.

LaTeX

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

Lean4

@[simp]
theorem mul_invOf_cancel_left' [Monoid α] (a b : α) {_ : Invertible a} : a * (⅟a * b) = b := by
  rw [← mul_assoc, mul_invOf_self, one_mul]

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

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

Разделы

Аффилиация

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