Skip to main content

LeftOrderedGroup

typeclass G: LeftOrderedGroup extends Group, LinearOrder {
    left_invariance(a: G, b: G, c: G) {
        a <= b implies c * a <= c * b
    }
}

A left-ordered group is a group with a left-invariant order. This means that if a <= b, then c * a <= c * b for any c in the group.

GitHub

antisymmetric​

Inherited from PartialOrder.

gt​

Inherited from PartialOrder.

gte​

Inherited from PartialOrder.

inverse​

Inherited from Group.

inverse_right​

Inherited from Group.

left_invariance​

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

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

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.

totality​

Inherited from LinearOrder.

transitive​

Inherited from PartialOrder.