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_reducible]

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

Equations

• Prod.instMulZeroClass = { toMul := Prod.instMul, toZero := Prod.instZero, zero_mul := ⋯, mul_zero := ⋯ }

@[instance_reducible]

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

Equations

• Prod.instSemigroupWithZero = { toSemigroup := Prod.instSemigroup, toZero := Prod.instZero, zero_mul := ⋯, mul_zero := ⋯ }

@[instance_reducible]

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

Equations

• Prod.instMulZeroOneClass = { toMulOneClass := Prod.instMulOneClass, toZero := Prod.instZero, zero_mul := ⋯, mul_zero := ⋯ }

@[instance_reducible]

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

Equations

• Prod.instMonoidWithZero = { toMonoid := Prod.instMonoid, toZero := Prod.instZero, zero_mul := ⋯, mul_zero := ⋯ }

@[instance_reducible]

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

Equations

• Prod.instCommMonoidWithZero = { toCommMonoid := Prod.instCommMonoid, toZero := Prod.instZero, zero_mul := ⋯, mul_zero := ⋯ }

@[simp]

theorem WithZero.coe_withZeroUnitsEquiv (M₀ : Type u_1) [GroupWithZero M₀] [DecidablePred fun (x : M₀) => x = 0] : ↑withZeroUnitsEquiv = lift' (Units.coeHom M₀)

@[deprecated WithZero.coe_withZeroUnitsEquiv (since := "2026-09-15")]

theorem WithZero.ofClass_withZeroUnitsEquiv (M₀ : Type u_1) [GroupWithZero M₀] [DecidablePred fun (x : M₀) => x = 0] : ↑withZeroUnitsEquiv = lift' (Units.coeHom M₀)

Alias of WithZero.coe_withZeroUnitsEquiv.

Multiplication and division as homomorphisms

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' := ⋯ }

@[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.

Equations

• divMonoidWithZeroHom = { toFun := (↑divMonoidHom).toFun, map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

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