English
There is an inverse operation on the coproduct of two groups, defined via the quotient map that reverses word order and replaces each letter by its inverse.
Русский
На копродукте двух групп существует обратная операция, определяемая через квазиобразование, которое разворачивает порядок слов и заменяет каждую букву на её обратную.
LaTeX
$$$\text{instance: Inv}(G \ast H) \text{ defined by } inv(x) = \mathrm{mk}(\text{ofList} (x.toList.map (\mathrm{Sum.mapInvInv}.inv))).$$$
Lean4
@[to_additive]
instance : Inv (G ∗ H) where
inv :=
Quotient.map' (fun w => ofList (w.toList.map (Sum.map Inv.inv Inv.inv)).reverse) fun _ _ ↦
(coprodCon G H).map_of_mul_left_rel_one _ con_inv_mul_cancel
