Skip to main content

Subring

structure Subring[R: Ring] {
    contains: R -> Bool
} constraint {
    subring_constraint(contains)
}

A subring of a ring, represented as a subset containing zero and one and closed under ring operations.

GitHub

as_set​

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

The subset of ring elements belonging to this subring.

closure​

let closure: Set[R] -> Subring[R] = subring_closure

The smallest subring containing a set.

contains​

Subring.contains: (Subring[R], R) -> Bool

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

ext​

let ext = subring_ext[R]

Subring extensionality from pointwise equality of membership.

intersection​

let intersection: (Subring[R], Subring[R]) -> Subring[R] = subring_intersection

The common part of two subrings.

sup​

let sup: (Subring[R], Subring[R]) -> Subring[R] = subring_sup

The least subring containing this subring and another subring.