inv_mul_cancel_left — Mathlib

English

In a DivisionMonoid, if a is a unit, then (a^{-1})·(a·b) = b for all b.

Русский

В делимом моноиде, если a единица, то (a^{-1})·(a·b) = b для любого b.

LaTeX

$$$\forall {\alpha} [DivisionMonoid\ \alpha] {a} (ha : IsUnit a) \forall (b : \alpha), (a^{-1}) \cdot (a \cdot b) = b$$$

Lean4

@[to_additive (attr := simp)]
protected theorem inv_mul_cancel_left (h : IsUnit a) : ∀ b, a⁻¹ * (a * b) = b :=
  h.unit'.inv_mul_cancel_left

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