Skip to main content

Group

typeclass G: Group extends Monoid {
    inverse: G -> G
    inverse_right(a: G) {
        a * a.inverse = G.1
    }
}

A group is a monoid that also has inverses.

GitHub

inverse​

inverse: G -> G

The inverse operation

inverse_right​

inverse_right(a: G) {
    a * a.inverse = G.1
}

We only need right-inverse; we can prove left-inverse from it.

mul​

Inherited from Semigroup.

mul_associative​

Inherited from Semigroup.

mul_identity_left​

Inherited from Monoid.

mul_identity_right​

Inherited from Monoid.