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_reducible]
instance Prod.instMulZeroClass {M₀ : Type u_1} {N₀ : Type u_2} [MulZeroClass M₀] [MulZeroClass N₀] :
MulZeroClass (M₀ × N₀)
source
@[instance_reducible]
instance Prod.instSemigroupWithZero {M₀ : Type u_1} {N₀ : Type u_2} [SemigroupWithZero M₀] [SemigroupWithZero N₀] :
SemigroupWithZero (M₀ × N₀)
source
@[instance_reducible]
instance Prod.instMulZeroOneClass {M₀ : Type u_1} {N₀ : Type u_2} [MulZeroOneClass M₀] [MulZeroOneClass N₀] :
MulZeroOneClass (M₀ × N₀)
source
@[instance_reducible]
instance Prod.instMonoidWithZero {M₀ : Type u_1} {N₀ : Type u_2} [MonoidWithZero M₀] [MonoidWithZero N₀] :
MonoidWithZero (M₀ × N₀)
source
@[instance_reducible]
instance Prod.instCommMonoidWithZero {M₀ : Type u_1} {N₀ : Type u_2} [CommMonoidWithZero M₀] [CommMonoidWithZero N₀] :
CommMonoidWithZero (M₀ × N₀)
source
@[simp]
theorem WithZero.coe_withZeroUnitsEquiv (M₀ : Type u_1) [GroupWithZero M₀] [DecidablePred fun (x : M₀) => x = 0] :
↑withZeroUnitsEquiv = lift' (Units.coeHom M₀)
source
@[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 #

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

Multiplication as a multiplicative homomorphism with zero.

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.

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