Adjoining a zero to a semiring

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

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

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

Equations

• WithZero.instDistrib = { toMul := MulZeroClass.toMul, toAdd := WithZero.instAdd, left_distrib := ⋯, right_distrib := ⋯ }

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

Equations

• One or more equations did not get rendered due to their size.