English
In the coproduct of groups, the inverse is given by applying the componentwise inverses after lifting and then conjugating by MulOpposite; the inverse of x is x^{-1} expressed via lift, of, and MulEquiv.inv'.
Русский
В копродукте групп обратное выражается через компонентные обратные после подъема и преобразования через MulEquiv.inv': обратное к x записано через lift и of.
LaTeX
$$$ x^{-1} = \\mathrm{MulOpposite.unop} \\Big( \\mathrm{lift}\\big(\\lambda i, (\\mathrm{of}: G_i \\to^* _).op \\cdot (\\mathrm{MulEquiv.inv'}(G_i)).toMonoidHom \\big) x \\Big)$$$
Lean4
theorem inv_def (x : CoprodI G) :
x⁻¹ = MulOpposite.unop (lift (fun i => (of : G i →* _).op.comp (MulEquiv.inv' (G i)).toMonoidHom) x) :=
rfl
