mul_inv_cancel_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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