Skip to main content

OrderedGroup

typeclass G: OrderedGroup extends LeftOrderedGroup {
    right_invariance(a: G, b: G, c: G) {
        a <= b implies a * c <= b * c
    }
}

An ordered group has both left and right invariance of the order under multiplication.

GitHub

antisymmetric​

Inherited from PartialOrder.

gt​

Inherited from PartialOrder.

gte​

Inherited from PartialOrder.

inverse​

Inherited from Group.

inverse_right​

Inherited from Group.

left_invariance​

Inherited from LeftOrderedGroup.

lt​

Inherited from PartialOrder.

lte​

Inherited from PartialOrder.

max​

Inherited from LinearOrder.

min​

Inherited from LinearOrder.

mul​

Inherited from Semigroup.

mul_associative​

Inherited from Semigroup.

mul_identity_left​

Inherited from Monoid.

mul_identity_right​

Inherited from Monoid.

reflexive​

Inherited from PartialOrder.

right_invariance​

right_invariance(a: G, b: G, c: G) {
    a <= b implies a * c <= b * c
}

Right multiplication preserves the order relation: if a ≤ b, then a * c ≤ b * c.

totality​

Inherited from LinearOrder.

transitive​

Inherited from PartialOrder.