English
There is a canonical equivalence between MulEquiv G H and AddEquiv (Additive G) (Additive H) via a left-action of adding and mapping between additive and multiplicative structures.
Русский
Существует каноническое эквивалентное соответствие между MulEquiv G H и AddEquiv (Additive G) (Additive H) через левое преобразование между аддитивной и умножительной структурами.
LaTeX
$$$\\mathrm{MulEquiv}(G,H) \\simeq \\mathrm{AddEquiv}( \\mathrm{Additive} G, \\mathrm{Additive} H)$$$
Lean4
/-- Reinterpret `G ≃* H` as `Additive G ≃+ Additive H`. -/
@[simps]
def toAdditive [MulOneClass G] [MulOneClass H] : G ≃* H ≃ (Additive G ≃+ Additive H)
where
toFun
f :=
{ toFun := MonoidHom.toAdditive f.toMonoidHom
invFun := MonoidHom.toAdditive f.symm.toMonoidHom
left_inv := f.left_inv
right_inv := f.right_inv
map_add' := map_mul f }
invFun
f :=
{ toFun := MonoidHom.toAdditive.symm f.toAddMonoidHom
invFun := MonoidHom.toAdditive.symm f.symm.toAddMonoidHom
left_inv := f.left_inv
right_inv := f.right_inv
map_mul' := map_add f }
