instMulOneClass — Mathlib

English

If α is a monoid, then the set of units αˣ carries a multiplicative monoid structure inherited from α, with the unit element being 1.

Русский

Если α — моноид, то множество обратимых элементов αˣ наделено умноженной моноидной структурой, наследуемой от α, тождество — единица 1.

LaTeX

$$$\operatorname{Monoid}(\alpha^{\times})$$$

Lean4

/-- Units of a monoid have a multiplication and multiplicative identity. -/
@[to_additive /-- Additive units of an additive monoid have an addition and an additive identity. -/
    ]
instance instMulOneClass : MulOneClass αˣ
    where
  one_mul u := ext <| one_mul (u : α)
  mul_one u := ext <| mul_one (u : α)

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