Skip to main content

AddOrderedGroup

typeclass G: AddOrderedGroup extends AddLeftOrderedGroup {
    right_invariance(a: G, b: G, c: G) {
        a <= b implies a + c <= b + c
    }
}

An ordered group has both left and right invariance.

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​

Inherited from AddLeftOrderedGroup.

lt​

Inherited from PartialOrder.

lte​

Inherited from LTE.

max​

Inherited from LinearOrder.

min​

Inherited from LinearOrder.

neg​

Inherited from Neg.

reflexive​

Inherited from PartialOrder.

right_invariance​

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

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

sub​

Inherited from AddGroup.

totality​

Inherited from LinearOrder.

transitive​

Inherited from PartialOrder.