Documentation

Mathlib.Algebra.GroupWithZero.Submonoid.Instances

Instances for the range submonoid of a monoid with zero hom #

source
@[instance_reducible]
instance MonoidWithZeroHom.instMulZeroOneClassSubtypeMemSubmonoidMrange {G : Type u_1} {H : Type u_2} [MulZeroOneClass G] [MulZeroOneClass H] (f : G →*₀ H) :
MulZeroOneClass ↥(MonoidHom.mrange f)
source
@[simp]
theorem MonoidWithZeroHom.val_mrange_zero {G : Type u_1} {H : Type u_2} [MulZeroOneClass G] [MulZeroOneClass H] (f : G →*₀ H) :
↑0 = 0
source
@[instance_reducible]
instance MonoidWithZeroHom.instMonoidWithZeroSubtypeMemSubmonoidMrange {G : Type u_1} {H : Type u_2} [MulZeroOneClass G] [MonoidWithZero H] (f : G →*₀ H) :
MonoidWithZero ↥(MonoidHom.mrange f)
source
@[instance_reducible]
instance MonoidWithZeroHom.instCommMonoidWithZeroSubtypeMemSubmonoidMrange {G : Type u_1} {H : Type u_2} [MulZeroOneClass G] [CommMonoidWithZero H] (f : G →*₀ H) :
CommMonoidWithZero ↥(MonoidHom.mrange f)
source
@[instance_reducible]
instance MonoidWithZeroHom.instGroupWithZeroSubtypeMemSubmonoidMrange {G : Type u_1} {H : Type u_2} [GroupWithZero G] [GroupWithZero H] (f : G →*₀ H) :
GroupWithZero ↥(MonoidHom.mrange f)
source
@[instance_reducible]
instance MonoidWithZeroHom.instCommGroupWithZeroSubtypeMemSubmonoidMrange {G : Type u_1} {H : Type u_2} [GroupWithZero G] [CommGroupWithZero H] (f : G →*₀ H) :
CommGroupWithZero ↥(MonoidHom.mrange f)
source
theorem MonoidWithZeroHom.mker_inverse {H : Type u_2} [CommGroupWithZero H] :
MonoidHom.mker MonoidWithZero.inverse = ⊥