Isomorphisms of monoids with zero #
@[instance 100]
instance
MulEquivClass.toZeroHomClass
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[EquivLike F α β]
[MulZeroClass α]
[MulZeroClass β]
[MulEquivClass F α β]
:
ZeroHomClass F α β
@[instance 100]
instance
MulEquivClass.toMonoidWithZeroHomClass
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[EquivLike F α β]
[MulZeroOneClass α]
[MulZeroOneClass β]
[MulEquivClass F α β]
:
MonoidWithZeroHomClass F α β