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 #

source
instance Prod.instMulZeroClass {M₀ : Type u_1} {N₀ : Type u_2} [MulZeroClass M₀] [MulZeroClass N₀] :
MulZeroClass (M₀ × N₀)
Equations
source
instance Prod.instSemigroupWithZero {M₀ : Type u_1} {N₀ : Type u_2} [SemigroupWithZero M₀] [SemigroupWithZero N₀] :
SemigroupWithZero (M₀ × N₀)
Equations
source
instance Prod.instMulZeroOneClass {M₀ : Type u_1} {N₀ : Type u_2} [MulZeroOneClass M₀] [MulZeroOneClass N₀] :
MulZeroOneClass (M₀ × N₀)
Equations
source
instance Prod.instMonoidWithZero {M₀ : Type u_1} {N₀ : Type u_2} [MonoidWithZero M₀] [MonoidWithZero N₀] :
MonoidWithZero (M₀ × N₀)
Equations
source
instance Prod.instCommMonoidWithZero {M₀ : Type u_1} {N₀ : Type u_2} [CommMonoidWithZero M₀] [CommMonoidWithZero N₀] :
CommMonoidWithZero (M₀ × N₀)
Equations

Multiplication and division as homomorphisms #

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

Multiplication as a multiplicative homomorphism with zero.

Equations
  • mulMonoidWithZeroHom = { toFun := (↑mulMonoidHom).toFun, map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯ }
Instances For
    source
    @[simp]
    theorem mulMonoidWithZeroHom_apply {M₀ : Type u_1} [CommMonoidWithZero M₀] :
    ∀ (a : M₀ × M₀), mulMonoidWithZeroHom a = (↑mulMonoidHom).toFun a
    source
    def divMonoidWithZeroHom {M₀ : Type u_1} [CommGroupWithZero M₀] :
    M₀ × M₀ →*₀ M₀

    Division as a multiplicative homomorphism with zero.

    Equations
    • divMonoidWithZeroHom = { toFun := (↑divMonoidHom).toFun, map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯ }
    Instances For
      source
      @[simp]
      theorem divMonoidWithZeroHom_apply {M₀ : Type u_1} [CommGroupWithZero M₀] :
      ∀ (a : M₀ × M₀), divMonoidWithZeroHom a = (↑divMonoidHom).toFun a