Skip to main content

AddSubmonoid

structure AddSubmonoid[M: AddMonoid] {
    contains: M -> Bool
} constraint {
    add_submonoid_constraint(contains)
}

An additive submonoid of an additive monoid, represented as a subset containing zero and closed under addition.

GitHub

as_set​

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

The subset of additive monoid elements belonging to this additive submonoid.

closure​

let closure: Set[M] -> AddSubmonoid[M] = add_submonoid_closure

The smallest additive submonoid containing a set.

contains​

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

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

ext​

let ext = add_submonoid_ext[M]

Additive submonoid extensionality from pointwise equality of membership.

intersection​

let intersection: (AddSubmonoid[M], AddSubmonoid[M]) -> AddSubmonoid[M] = add_submonoid_intersection

The common part of two additive submonoids.

sup​

let sup: (AddSubmonoid[M], AddSubmonoid[M]) -> AddSubmonoid[M] = add_submonoid_sup

The least additive submonoid containing this additive submonoid and another additive submonoid.