mathlib3 documentation

algebra.order.monoid.to_mul_bot

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Making an additive monoid multiplicative then adding a zero is the same as adding a bottom element then making it multiplicative.

Making an additive monoid multiplicative then adding a zero is the same as adding a bottom element then making it multiplicative.

Equations