The units of an ordered commutative monoid form an ordered commutative group

instance Units.orderedCommGroup {α : Type u_1} [OrderedCommMonoid α] : OrderedCommGroup αˣ

The units of an ordered commutative monoid form an ordered commutative group.

Equations

• Units.orderedCommGroup = OrderedCommGroup.mk ⋯

instance AddUnits.orderedAddCommGroup {α : Type u_1} [OrderedAddCommMonoid α] : OrderedAddCommGroup (AddUnits α)

The units of an ordered commutative additive monoid form an ordered commutative additive group.

Equations

• AddUnits.orderedAddCommGroup = OrderedAddCommGroup.mk ⋯

instance Units.instLinearOrderedCommGroup {α : Type u_1} [LinearOrderedCommMonoid α] : LinearOrderedCommGroup αˣ

The units of a linearly ordered commutative monoid form a linearly ordered commutative group.

Equations

• Units.instLinearOrderedCommGroup = LinearOrderedCommGroup.mk ⋯ LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT ⋯ ⋯ ⋯

instance AddUnits.instLinearOrderedAddCommGroup {α : Type u_1} [LinearOrderedAddCommMonoid α] : LinearOrderedAddCommGroup (AddUnits α)

The units of a linearly ordered commutative additive monoid form a linearly ordered commutative additive group.

Equations

• AddUnits.instLinearOrderedAddCommGroup = LinearOrderedAddCommGroup.mk ⋯ LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT ⋯ ⋯ ⋯