Documentation

Mathlib.Algebra.Ring.WithZero

Adjoining a zero to a semiring #

source
📐 coverage
instance WithZero.instLeftDistribClass {α : Type u_1} [Mul α] [Add α] [LeftDistribClass α] :
LeftDistribClass (WithZero α)
source
📐 coverage
instance WithZero.instRightDistribClass {α : Type u_1} [Mul α] [Add α] [RightDistribClass α] :
RightDistribClass (WithZero α)
source
🔸 coverage
@[implicit_reducible]
instance WithZero.instDistrib {α : Type u_1} [Distrib α] :
Distrib (WithZero α)
source
🔸 coverage
@[implicit_reducible]
instance WithZero.instSemiring {α : Type u_1} [Semiring α] :
Semiring (WithZero α)