Skip to main content

Monoid

typeclass M: Monoid extends Semigroup, One {
    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 Mul.

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.

pow​

define pow(self, exp: Nat) -> M {
    match exp {
        Nat.zero {
            M.1
        }
        Nat.suc(n) {
            self * self.pow(n)
        }
    }
}

Raises a monoid element to a natural number power using repeated multiplication.