Skip to main content

AddGroup

typeclass A: AddGroup extends AddMonoid {
    neg: A -> A
    inverse_right(a: A) {
        a + -a = A.0
    }
}

An additive group is an additive monoid that also has inverses.

GitHub

add​

Inherited from AddSemigroup.

add_associative​

Inherited from AddSemigroup.

add_identity_left​

Inherited from AddMonoid.

add_identity_right​

Inherited from AddMonoid.

inverse_right​

inverse_right(a: A) {
    a + -a = A.0
}

This is what "additive inverse" means.

neg​

neg: A -> A

The additive inverse of an element.

sub​

define sub(self, other: A) -> A {
    self + -other
}

Subtracts one element from another using additive inverse.