inv_mul_cancel_right

Mathlib.Algebra.Group.Units.Basic

URI: https://scilib.ai/kg/mathlib#Units.inv_mul_cancel_right

English

In a monoid, for any unit a, b·a = c·a iff b = c.

Русский

В моноиде для любого единичного элемента a справедливо: b·a = c·a эквивалентно b = c.

LaTeX

$$$\forall a\in \alpha^{\times},\; \forall b,c\in \alpha:\; b a = c a \iff b = c$$$

Lean4

@[to_additive (attr := simp)]
theorem inv_mul_cancel_right (a : α) (b : αˣ) : a * ↑b⁻¹ * b = a := by rw [mul_assoc, inv_mul, mul_one]

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

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

Разделы

Аффилиация

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