Documentation

Mathlib.Algebra.GroupWithZero.Submonoid.Instances

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

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