# Isomorphisms of monoids with zero #

source
@[instance 100]
instance MulEquivClass.toZeroHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [EquivLike F α β] [MulZeroClass α] [MulZeroClass β] [MulEquivClass F α β] :
ZeroHomClass F α β
source
@[instance 100]
instance MulEquivClass.toMonoidWithZeroHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [EquivLike F α β] [MulZeroOneClass α] [MulZeroOneClass β] [MulEquivClass F α β] :
MonoidWithZeroHomClass F α β
source
def MulEquiv.toMonoidWithZeroHom {G : Type u_1} {H : Type u_2} [MulZeroOneClass G] [MulZeroOneClass H] (f : G ≃* H) :
G →*₀ H

An isomorphism of monoids with zero can be treated as a homomorphism preserving zero. This is a helper projection that utilizes the `MonoidWithZeroHomClass` instance.

Equations

- f.toMonoidWithZeroHom = ↑f

Instances For

source
@[simp]
theorem MulEquiv.toMonoidWithZeroHom_apply {G : Type u_1} {H : Type u_2} [MulZeroOneClass G] [MulZeroOneClass H] (f : G ≃* H) (x : G) :
f.toMonoidWithZeroHom x = f x
source
theorem MulEquiv.toMonoidWithZeroHom_injective {G : Type u_1} {H : Type u_2} [MulZeroOneClass G] [MulZeroOneClass H] (f : G ≃* H) :
Function.Injective ⇑f.toMonoidWithZeroHom
source
theorem MulEquiv.toMonoidWithZeroHom_surjective {G : Type u_1} {H : Type u_2} [MulZeroOneClass G] [MulZeroOneClass H] (f : G ≃* H) :
Function.Surjective ⇑f.toMonoidWithZeroHom
source
theorem MulEquiv.toMonoidWithZeroHom_bijective {G : Type u_1} {H : Type u_2} [MulZeroOneClass G] [MulZeroOneClass H] (f : G ≃* H) :
Function.Bijective ⇑f.toMonoidWithZeroHom
source
@[simp]
theorem MulEquiv.toMonoidWithZeroHom_inj {G : Type u_1} {H : Type u_2} [MulZeroOneClass G] [MulZeroOneClass H] {f g : G ≃* H} :
f.toMonoidWithZeroHom = g.toMonoidWithZeroHom ↔ f = g