invertible — Mathlib

English

Units are invertible in their associated monoid; each unit has a two-sided inverse.

Русский

Единицы обратимы в связном моноиде; для каждой единицы существует обратное слева и справа.

LaTeX

$$$ \forall u \in \mathsf{Units}(\alpha), \; u \text{ is invertible in } \alpha$$$

Lean4

/-- Units are invertible in their associated monoid. -/
instance invertible [Monoid α] (u : αˣ) : Invertible (u : α)
    where
  invOf := ↑u⁻¹
  invOf_mul_self := u.inv_mul
  mul_invOf_self := u.mul_inv

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