English
A dual construction provides an equivalence between MulEquiv and AddEquiv via the right Additive functor, reflecting symmetry between left and right actions.
Русский
Двойная конструкция даёт эквиваленцию между MulEquiv и AddEquiv через правый аддитивный функтор, отражая симметрию между левыми и правыми действиями.
LaTeX
$$$\\mathrm{MulEquiv}(G,H) \\simeq \\mathrm{AddEquiv}(G, \\mathrm{Additive} H)$$$
Lean4
/-- Reinterpret `G ≃+ Additive H` as `Multiplicative G ≃* H`. -/
@[simps]
def toMultiplicativeLeft [AddZeroClass G] [MulOneClass H] : G ≃+ Additive H ≃ (Multiplicative G ≃* H)
where
toFun
f :=
{ toFun := f.toAddMonoidHom.toMultiplicativeLeft
invFun := f.symm.toAddMonoidHom.toMultiplicativeRight
left_inv := f.left_inv
right_inv := f.right_inv
map_mul' := map_add f }
invFun
f :=
{ toFun := f.toMonoidHom.toAdditiveRight
invFun := f.symm.toMonoidHom.toAdditiveLeft
left_inv := f.left_inv
right_inv := f.right_inv
map_add' := map_mul f }
