instGroupSubtypeMemSubmonoid — Mathlib

English

The unitary elements of a star-monoid form a group under multiplication, with inverse given by the star operation.

Русский

Унитарные элементы звёздованного моноида образуют группу под умножением; обратный элемент задаётся операцией звезды.

LaTeX

$$$ \mathrm{Unitary}(R) \, \text{ is a group under } \cdot \text{ with } (U)^{-1} = \star U $$$

Lean4

instance : Group (unitary R) :=
  { Submonoid.toMonoid _ with
    inv := star
    inv_mul_cancel := star_mul_self }

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