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₀] :
MulZeroClass (M₀ × N₀)
Equations
instance Prod.instSemigroupWithZero {M₀ : Type u_1} {N₀ : Type u_2} [SemigroupWithZero M₀] [SemigroupWithZero N₀] :
SemigroupWithZero (M₀ × N₀)
Equations
instance Prod.instMulZeroOneClass {M₀ : Type u_1} {N₀ : Type u_2} [MulZeroOneClass M₀] [MulZeroOneClass N₀] :
MulZeroOneClass (M₀ × N₀)
Equations
instance Prod.instMonoidWithZero {M₀ : Type u_1} {N₀ : Type u_2} [MonoidWithZero M₀] [MonoidWithZero N₀] :
MonoidWithZero (M₀ × N₀)
Equations
instance Prod.instCommMonoidWithZero {M₀ : Type u_1} {N₀ : Type u_2} [CommMonoidWithZero M₀] [CommMonoidWithZero N₀] :
Equations

Multiplication and division as homomorphisms #

@[simp]
theorem mulMonoidWithZeroHom_apply {M₀ : Type u_1} [CommMonoidWithZero M₀] :
∀ (a : M₀ × M₀), mulMonoidWithZeroHom a = (↑mulMonoidHom).toFun a
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
    @[simp]
    theorem divMonoidWithZeroHom_apply {M₀ : Type u_1} [CommGroupWithZero M₀] :
    ∀ (a : M₀ × M₀), divMonoidWithZeroHom a = (↑divMonoidHom).toFun a
    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