inv_smul — Mathlib

English

If a is a unit in a monoid, then its inverse acts as the multiplicative identity on any element.

Русский

Если a — единица в моноиде, то её обратное действует как единица на любом элементе.

LaTeX

$$$ \\text{IsUnit } a \\Rightarrow a^{-1} \\cdot x = 1 \\quad \\text{for all } x$$$

Lean4

@[to_additive]
theorem _root_.IsUnit.inv_smul [Monoid α] {a : α} (h : IsUnit a) : h.unit⁻¹ • a = 1 :=
  h.val_inv_mul

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