Adjoining a zero to a semiring

instance WithZero.instLeftDistribClass {α : Type u_1} [Mul α] [Add α] [LeftDistribClass α] : LeftDistribClass (WithZero α)

Equations

• ⋯ = ⋯

instance WithZero.instRightDistribClass {α : Type u_1} [Mul α] [Add α] [RightDistribClass α] : RightDistribClass (WithZero α)

Equations

• ⋯ = ⋯

instance WithZero.instDistrib {α : Type u_1} [Distrib α] : Distrib (WithZero α)

Equations

• WithZero.instDistrib = Distrib.mk ⋯ ⋯

instance WithZero.instSemiring {α : Type u_1} [Semiring α] : Semiring (WithZero α)

Equations

• WithZero.instSemiring = Semiring.mk ⋯ ⋯ ⋯ ⋯ Monoid.npow ⋯ ⋯