Adjoining a zero to a semiring

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

Equations

• (_ : LeftDistribClass (WithZero α)) = (_ : LeftDistribClass (WithZero α))

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

Equations

• (_ : RightDistribClass (WithZero α)) = (_ : RightDistribClass (WithZero α))

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

Equations

• WithZero.instDistrib = Distrib.mk (_ : ∀ (a b c : WithZero α), a * (b + c) = a * b + a * c) (_ : ∀ (a b c : WithZero α), (a + b) * c = a * c + b * c)

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

Equations

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