Documentation

Mathlib.Algebra.GroupWithZero.Prod

Products of monoids with zero, groups with zero #

In this file we define MonoidWithZero, GroupWithZero, etc... instances for M₀ × N₀.

Main declarations #

instance Prod.instMulZeroClass {M₀ : Type u_1} {N₀ : Type u_2} [MulZeroClass M₀] [MulZeroClass N₀] :
Equations

Multiplication and division as homomorphisms #

def mulMonoidWithZeroHom {M₀ : Type u_1} [CommMonoidWithZero M₀] :
M₀ × M₀ →*₀ M₀

Multiplication as a multiplicative homomorphism with zero.

Equations
Instances For
    @[simp]
    theorem mulMonoidWithZeroHom_apply {M₀ : Type u_1} [CommMonoidWithZero M₀] (a✝ : M₀ × M₀) :
    def divMonoidWithZeroHom {M₀ : Type u_1} [CommGroupWithZero M₀] :
    M₀ × M₀ →*₀ M₀

    Division as a multiplicative homomorphism with zero.

    Equations
    Instances For
      @[simp]
      theorem divMonoidWithZeroHom_apply {M₀ : Type u_1} [CommGroupWithZero M₀] (a✝ : M₀ × M₀) :