Skip to main content

Ideal

structure Ideal[R: CommRing] {
    contains: R -> Bool
} constraint {
    is_ideal(contains)
}

An ideal of a commutative ring, represented as a subset closed under addition and absorbing multiplication.

GitHub

as_set​

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

The subset of ring elements belonging to this ideal.

closure​

let closure: Set[R] -> Ideal[R] = ideal_closure

The smallest ideal containing a set.

contains​

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

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

ext​

let ext = ideal_ext[R]

Ideal extensionality from pointwise equality of membership.

intersection​

let intersection: (Ideal[R], Ideal[R]) -> Ideal[R] = bundled_ideal_inter

The common part of two ideals.

principal​

let principal: R -> Ideal[R] = bundled_principal_ideal

The principal ideal generated by an element.

sum​

let sum: (Ideal[R], Ideal[R]) -> Ideal[R] = bundled_ideal_sum

The least ideal containing two ideals.

unit​

let unit = bundled_unit_ideal[R]

The unit ideal.

zero​

let zero = bundled_zero_ideal[R]

The zero ideal.