Products of monoids with zero, groups with zero

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

Main declarations

• mulMonoidWithZeroHom: Multiplication bundled as a monoid with zero homomorphism.
• divMonoidWithZeroHom: Division bundled as a monoid with zero homomorphism.

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

instance Prod.instSemigroupWithZero {M₀ : Type u_1} {N₀ : Type u_2} [SemigroupWithZero M₀] [SemigroupWithZero N₀] : SemigroupWithZero (M₀ × N₀)

instance Prod.instMulZeroOneClass {M₀ : Type u_1} {N₀ : Type u_2} [MulZeroOneClass M₀] [MulZeroOneClass N₀] : MulZeroOneClass (M₀ × N₀)

instance Prod.instMonoidWithZero {M₀ : Type u_1} {N₀ : Type u_2} [MonoidWithZero M₀] [MonoidWithZero N₀] : MonoidWithZero (M₀ × N₀)

instance Prod.instCommMonoidWithZero {M₀ : Type u_1} {N₀ : Type u_2} [CommMonoidWithZero M₀] [CommMonoidWithZero N₀] : CommMonoidWithZero (M₀ × N₀)

Multiplication and division as homomorphisms

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

Multiplication as a multiplicative homomorphism with zero.

@[simp]

theorem mulMonoidWithZeroHom_apply {M₀ : Type u_1} [CommMonoidWithZero M₀] (a✝ : M₀ × M₀) : mulMonoidWithZeroHom a✝ = (↑mulMonoidHom).toFun a✝

def divMonoidWithZeroHom {M₀ : Type u_1} [CommGroupWithZero M₀] : M₀ × M₀ →*₀ M₀

Division as a multiplicative homomorphism with zero.

@[simp]

theorem divMonoidWithZeroHom_apply {M₀ : Type u_1} [CommGroupWithZero M₀] (a✝ : M₀ × M₀) : divMonoidWithZeroHom a✝ = (↑divMonoidHom).toFun a✝