English
If α has a representation, then αˣ inherits a representation given by composing the representation with the underlying value map: repr_{αˣ}(u) = repr_α(val(u)).
Русский
Если у α есть представление, то у αˣ появляется представление, задаваемое через составку: repr_{αˣ}(u) = repr_α(u.val).
LaTeX
$$$\operatorname{repr}_{\alpha^{\times}}(u) = \operatorname{repr}_{\alpha}(u_{\mathrm{val}})$$$
Lean4
/-- Units of a monoid have a representation of the base value in the `Monoid`. -/
@[to_additive /-- Additive units of an additive monoid have a representation of the base value in
the `AddMonoid`. -/
]
instance [Repr α] : Repr αˣ :=
⟨reprPrec ∘ val⟩
