Structures · Algebra

LinearOrderedCommMonoidWithZero

A linearly ordered commutative monoid with a zero element.

Defined in: Mathlib.Algebra.Order.GroupWithZero.Canonical
Shape: One type argument

Open in Mathlib docs

Extends5

Extended by1

LinearOrderedCommGroupWithZero

Concrete types that are instances5

Nat
Subtype
Set.Elem
Multiplicative
WithZero

How is a type an instance?

Loading the hierarchy index…

Assumed by163