Skip to main content

Monoid

typeclass M: Monoid extends Semigroup {
    1: M
    mul_identity_right(a: M) {
        a * M.1 = a
    }
    mul_identity_left(a: M) {
        M.1 * a = a
    }
}

A multiplicative monoid is a multiplicative semigroup with an identity element. Note that you need the identity to work on the right side as well as the left. One doesn't imply the other.

GitHub

mul​

Inherited from Semigroup.

mul_associative​

Inherited from Semigroup.

mul_identity_left​

mul_identity_left(a: M) {
    M.1 * a = a
}

The identity element must satisfy the identity property on the left.

mul_identity_right​

mul_identity_right(a: M) {
    a * M.1 = a
}

The identity element must satisfy the identity property on the right.