Skip to main content

AddLeftOrderedGroup

typeclass G: AddLeftOrderedGroup extends AddGroup, 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

add​

Inherited from Add.

add_associative​

Inherited from AddSemigroup.

add_identity_left​

Inherited from AddMonoid.

add_identity_right​

Inherited from AddMonoid.

antisymmetric​

Inherited from PartialOrder.

gt​

Inherited from PartialOrder.

gte​

Inherited from PartialOrder.

inverse_right​

Inherited from AddGroup.

left_invariance​

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

Left addition preserves the order relation: if a ≤ b, then c + a ≤ c + b.

lt​

Inherited from PartialOrder.

lte​

Inherited from LTE.

max​

Inherited from LinearOrder.

min​

Inherited from LinearOrder.

neg​

Inherited from Neg.

reflexive​

Inherited from PartialOrder.

sub​

Inherited from AddGroup.

totality​

Inherited from LinearOrder.

transitive​

Inherited from PartialOrder.