instGroup — Mathlib

English

The units α^× form a group under multiplication; the inverse is given by the inverse in α^× and underlying element is taken in α.

Русский

Единицы α^× образуют группу под умножением; обратный элемент берётся как обратный элемент в единицах, соответствующий элементу в α.

LaTeX

$$$\alpha^{\times} \text{ is a group under } \cdot$$$

Lean4

/-- Units of a monoid form a group. -/
@[to_additive /-- Additive units of an additive monoid form an additive group. -/
    ]
instance instGroup : Group αˣ where inv_mul_cancel := fun u => ext u.inv_val

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