Instances for the range submonoid of a monoid with zero hom

@[instance_reducible]

instance MonoidWithZeroHom.instMulZeroOneClassSubtypeMemSubmonoidMrange {G : Type u_1} {H : Type u_2} [MulZeroOneClass G] [MulZeroOneClass H] (f : G →*₀ H) : MulZeroOneClass ↥(MonoidHom.mrange f)

Equations

• f.instMulZeroOneClassSubtypeMemSubmonoidMrange = { toMulOneClass := (MonoidHom.mrange f).toMulOneClass, zero := ⟨0, ⋯⟩, zero_mul := ⋯, mul_zero := ⋯ }

@[simp]

theorem MonoidWithZeroHom.val_mrange_zero {G : Type u_1} {H : Type u_2} [MulZeroOneClass G] [MulZeroOneClass H] (f : G →*₀ H) : ↑0 = 0

@[instance_reducible]

instance MonoidWithZeroHom.instMonoidWithZeroSubtypeMemSubmonoidMrange {G : Type u_1} {H : Type u_2} [MulZeroOneClass G] [MonoidWithZero H] (f : G →*₀ H) : MonoidWithZero ↥(MonoidHom.mrange f)

Equations

• f.instMonoidWithZeroSubtypeMemSubmonoidMrange = { toMonoid := (MonoidHom.mrange f).toMonoid, toZero := f.instMulZeroOneClassSubtypeMemSubmonoidMrange.toZero, zero_mul := ⋯, mul_zero := ⋯ }

@[instance_reducible]

instance MonoidWithZeroHom.instCommMonoidWithZeroSubtypeMemSubmonoidMrange {G : Type u_1} {H : Type u_2} [MulZeroOneClass G] [CommMonoidWithZero H] (f : G →*₀ H) : CommMonoidWithZero ↥(MonoidHom.mrange f)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance MonoidWithZeroHom.instGroupWithZeroSubtypeMemSubmonoidMrange {G : Type u_1} {H : Type u_2} [GroupWithZero G] [GroupWithZero H] (f : G →*₀ H) : GroupWithZero ↥(MonoidHom.mrange f)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance MonoidWithZeroHom.instCommGroupWithZeroSubtypeMemSubmonoidMrange {G : Type u_1} {H : Type u_2} [GroupWithZero G] [CommGroupWithZero H] (f : G →*₀ H) : CommGroupWithZero ↥(MonoidHom.mrange f)

Equations

• One or more equations did not get rendered due to their size.

theorem MonoidWithZeroHom.mker_inverse {H : Type u_2} [CommGroupWithZero H] : MonoidHom.mker MonoidWithZero.inverse = ⊥