Skip to main content

Submonoid

structure Submonoid[M: Monoid] {
    contains: M -> Bool
} constraint {
    submonoid_constraint(contains)
}

A submonoid of a monoid M, represented as a subset closed under multiplication that contains the identity.

GitHub

as_set​

define as_set(self) -> Set[M] {
    Set[M].new(self.contains)
}

The subset of monoid elements belonging to this submonoid.

closure​

let closure: Set[M] -> Submonoid[M] = submonoid_closure

The smallest submonoid containing a set.

contains​

Submonoid.contains: (Submonoid[M], M) -> Bool

True if the given element is a member of this submonoid.

ext​

let ext = submonoid_ext[M]

Submonoid extensionality from pointwise equality of membership.

intersection​

let intersection: (Submonoid[M], Submonoid[M]) -> Submonoid[M] = submonoid_intersection

The common part of two submonoids.

sup​

let sup: (Submonoid[M], Submonoid[M]) -> Submonoid[M] = submonoid_sup

The least submonoid containing this submonoid and another submonoid.