# The Algebra Library (alglib)

Collection of algebraic operations.

## unary_relation#

unary_relation(D, ∼)


Returns true if ∼ is a unary relation over domain D.

#### Definition#

@inlinedef unary_relation(D, ∼) =    equal(arity[∼], 1)

## binary_relation#

binary_relation(D, ∼)


Returns true if ∼ is a binary relation over domain D.

#### Definition#

@inlinedef binary_relation(D, ∼) =    equal(arity[∼], 2)

## irreflexive#

irreflexive(D, ∼)


A binary relation is irreflexive if a ∼ a is never true for all a in D.

#### Definition#

@inlinedef irreflexive(D, ∼) =    binary_relation(D, ∼) and    forall(a ∈ D: ¬(a ∼ a))

## reflexive#

reflexive(D, ∼)


A binary relation is reflexive if a ∼ a is always true for all a in D.

#### Definition#

@inlinedef reflexive(D, ∼) =    binary_relation(D, ∼) and    forall(a ∈ D: a ∼ a)

## symmetric#

symmetric(D, ∼)


A binary relation is symmetric if for all a and b in D, whenever a ∼ b is true, then also b ∼ a is also true.

#### Definition#

@inlinedef symmetric(D, ∼) =    binary_relation(D, ∼) and    forall(a ∈ D, b ∈ D: a ∼ b ≡ b ∼ a)

## antisymmetric#

antisymmetric(D, ∼)


A binary relation is antisymmetric if for all a and b in D, whenever a ∼ b and b ∼ a are true, then b = a.

#### Definition#

@inlinedef antisymmetric(D, ∼) =    binary_relation(D, ∼) and    binary_relation_substitution_laws(D, ∼, =) and    forall(a ∈ D, b ∈ D: ((a ∼ b) and (b ∼ a)) ⇒ a = b)

## transitive#

transitive(D, ∼)


A binary relation is transitive if for all a, b and c in D, whenever a ∼ b and b ∼ c are true, then also a ∼ c is true.

#### Definition#

@inlinedef transitive(D, ∼) =    binary_relation(D, ∼) and    forall(a ∈ D, b ∈ D, c ∈ D: a ∼ b and b ∼ c implies a ∼ c)

## equivalence_relation#

equivalence_relation(D, ∼)


A binary relation is an equivalence_relation if it is reflexive, symmetric, and transitive

#### Definition#

@inlinedef equivalence_relation(D, ∼) =    reflexive(D, ∼) and symmetric(D, ∼) and transitive(D, ∼)

## unary_relation_substitution_laws#

unary_relation_substitution_laws(D, R, ≈)


A unary relation obeys substitution laws if the relation R produces the same results when values are substituted according to the binary relation ≈.

For example, unary_relation_substitution_laws({1; 2}, {1; 2}, (1, 2)) is true because the result of R(1) remains true when 1 is replaced by 2.

#### Definition#

@inlinedef unary_relation_substitution_laws(D, R, ≈) =    unary_relation(D, R) and binary_relation(D, ≈) and    forall(a ∈ D, b ∈ D: (a ≈ b) ⇒ (R(a) ≡ R(b)))

## binary_relation_substitution_laws#

binary_relation_substitution_laws(D, R, ≈)


A binary relation obeys substitution laws if the relation R produces the same results when values are substituted according to the binary relation ≈.

#### Definition#

@inlinedef binary_relation_substitution_laws(D, ∼, ≈) =    binary_relation(D, ∼) and binary_relation(D, ≈) and    forall(a1 ∈ D, a2 ∈ D: a1 ≈ a2 ⇒ forall(b ∈ D: a1 ∼ b ≡ a2 ∼ b)) and    forall(b1 ∈ D, b2 ∈ D: b1 ≈ b2 ⇒ forall(a ∈ D: a ∼ b1 ≡ a ∼ b2))

## partial_order#

preorder(D, ≼)


A binary relation ≼ is a preorder if it is reflexive and transitive.

#### Definition#

@inlinedef partial_order(D, ≼) =    reflexive(D, ≼) and transitive(D, ≼)

## partial_order#

partial_order(D, ≼)


A binary relation ≼ is a partial order if it is reflexive, antisymmetric, and transitive.

#### Definition#

@inlinedef partial_order(D, ≼) =    reflexive(D, ≼) and antisymmetric(D, ≼) and transitive(D, ≼)

## strict_partial_order#

strict_partial_order(D, ≺)


A binary relation ≺ is a strict partial order if it is irreflexive, antisymmetric, and transitive. This is similar to a partial order, but is irreflexive rather than reflexive.

#### Definition#

@inlinedef strict_partial_order(D, ≺) =    irreflexive(D, ≺) and antisymmetric(D, ≺) and transitive(D, ≺)

## comparable#

comparable(a, b, ≼)


Two elements a and b are comparable if either a ≼ b or b ≼ a.

#### Definition#

@inlinedef comparable(a, b, ≼) =    (a ≼ b) ∨ (b ≼ a)

## total_order#

total_order(D, ≼)


A binary relation ≼ is a total order if it is a partial order, and every element in D is comparable with every other element in D with respect to the partial order.

#### Definition#

@inlinedef total_order(D, ≼) =    partial_order(D, ≼) and    forall(a ∈ D, b ∈ D: comparable(a, b, ≼))

## strict_total_order#

strict_total_order(D, ≺)


A binary relation ≺ is a strict total order if it is a strict partial order, and every element in D is either comparable or equal to another element in D.

#### Definition#

@inlinedef strict_total_order(D, ≺) =    strict_partial_order(D, ≺) and    forall(a ∈ D, b ∈ D: comparable(a, b, ≺) ∨ (b = a))

## maximal_element#

maximal_element[D, ≼]


The maximal element of a partial order ≼ is an element which is greater than all other elements in D.

#### Definition#

@inlinedef maximal_element[D, ≼] =    max_elem: D(max_elem) and    partial_order(D, ≼) and    forall(a ∈ D: a ≼ max_elem)

## has_maximal_element#

has_maximal_element(D, ≼)


This returns true if the partial order ≼ contains a maximal element.

#### Definition#

@inlinedef has_maximal_element(D, ≼) =    partial_order(D, ≼) and    exists(max_elem ∈ D: forall(a ∈ D: a ≼ max_elem))

## minimal_element#

minimal_element[D, ≼]


The minimal element of a partial order ≼ is an element which is less than all other elements in D.

#### Definition#

@inlinedef minimal_element[D, ≼] =    min_elem: D(min_elem) and    partial_order(D, ≼) and    forall(a ∈ D: min_elem ≼ a)

## has_minimal_element#

has_minimal_element(D, ≼)


This returns true if the partial order ≼ contains a minimal element.

#### Definition#

@inlinedef has_minimal_element(D, ≼) =    partial_order(D, ≼) and    exists(min_elem ∈ D: forall(a ∈ D: min_elem ≼ a))

## unary_operator#

unary_operator(D, ⊙)


A unary operator takes one argument and returns another argument of the same type, i.e., it can be represented as a binary relation.

#### Definition#

@inlinedef unary_operator(D, ⊙) =    equal(arity[⊙], 2)

## binary_operator#

binary_operator(D, ⊙)


A binary operator takes two arguments and returns another argument of the same type, i.e., it can be represented as a relation of arity 3.

#### Definition#

@inlinedef binary_operator(D, ⊙) =    equal(arity[⊙], 3)

## approximately_commutative#

approximately_commutative(D, ⊙, ≈)


A binary operator ⊙ is approximately commutative if a ⊙ b is approximately equal to b ⊙ a for all a and b in D, where approximately equal is defined by the binary relation ≈.

#### Definition#

@inlinedef approximately_commutative(D, ⊙, ≈) =    binary_operator(D, ⊙) and    reflexive(D, ≈) and    symmetric(D, ≈) and    forall(a ∈ D, b ∈ D: (a ⊙ b) ≈ (b ⊙ a))

## commutative#

commutative(D, ⊙)


A binary operator ⊙ is commutative if a ⊙ b is equal to b ⊙ a for all a and b in D.

#### Definition#

@inlinedef commutative(D, ⊙) =    approximately_commutative(D, ⊙, =)

## approximately_associative#

approximately_associative(D, ⊙, ≈)


A binary operator ⊙ is approximately associative if (a ⊙ b) ⊙ c is approximately equal to a ⊙ (b ⊙ c) for all a, b and c in D, where approximately equal is defined by the binary relation ≈.

#### Definition#

@inlinedef approximately_associative(D, ⊙, ≈) =    binary_operator(D, ⊙) and    reflexive(D, ≈) and    symmetric(D, ≈) and    forall(a ∈ D, b ∈ D, c ∈ D: ((a ⊙ b) ⊙ c) ≈ (a ⊙ (b ⊙ c)))

## associative#

associative(D, ⊙)


A binary operator ⊙ is associative if (a ⊙ b) ⊙ c is equal to a ⊙ (b ⊙ c) for all a, b and c in D.

#### Definition#

@inlinedef associative(D, ⊙) =    approximately_associative(D, ⊙, =)

## idempotent#

idempotent(D, ⊙, ≈)


A binary operator ⊙ is idempotent if a ⊙ a = a for all a in D.

#### Definition#

@inlinedef idempotent(D, ⊙) =    binary_operator(D, ⊙) and    forall(a ∈ D: (a ⊙ a) = a)

## left_identity#

left_identity[D, ⊙]


A left identity of a binary operator ⊙ is an element i such that i ⊙ a = a for all a in D.

#### Definition#

@inlinedef left_identity[D, ⊙] =    ident: D(ident) and    forall(a ∈ D: ((ident ⊙ a) = a)) and    binary_operator(D, ⊙)

## has_left_identity#

has_left_identity(D, ⊙)


This returns true if ⊙ has a left identity.

#### Definition#

@inlinedef has_left_identity(D, ⊙) =    binary_operator(D, ⊙) and    equivalence_relation(D, =) and    // TODO: ideally we could do    // exists(ident ∈ D: left_identity[D, ⊙](ident))    // however this doesn't terminate    exists(ident ∈ D: forall(a ∈ D: ((ident ⊙ a) = a)))

## right_identity#

right_identity[D, ⊙]


A right identity of a binary operator ⊙ is an element i such that a ⊙ i = a for all a in D.

#### Definition#

@inlinedef right_identity[D, ⊙] =    ident: D(ident) and    forall(a ∈ D: ((a ⊙ ident) = a)) and    binary_operator(D, ⊙)

## has_right_identity#

has_right_identity(D, ⊙)


This returns true if ⊙ has a right identity.

#### Definition#

@inlinedef has_right_identity(D, ⊙) =    binary_operator(D, ⊙) and    exists(ident ∈ D: forall(a ∈ D: ((a ⊙ ident) = a)))

## identity#

identity[D, ⊙]


An identity of a binary operator ⊙ is both a left and right identity.

#### Definition#

@inlinedef identity[D, ⊙] =    ident: D(ident) and    left_identity[D, ⊙](ident) and right_identity[D, ⊙](ident)

## has_identity#

has_identity(D, ⊙)


This returns true if ⊙ has an identity.

#### Definition#

@inlinedef has_identity(D, ⊙) =    binary_operator(D, ⊙) and    exists(ident ∈ D: forall(a ∈ D: (a ⊙ ident) = a and (ident ⊙ a) = a))

## approximately_has_inverse#

approximately_has_inverse(D, ⊙, N, ≈)


For a binary relation ⊙, an inverse of an element a is an element b such that a ⊙ b is approximately equal to the identity element. For approximately_has_inverse, the inverse operator is given as N, so the inverse of a is N[a], and approximately equal to is defined by ≈.

#### Definition#

@inlinedef approximately_has_inverse(D, ⊙, N, ≈) =    binary_operator(D, ⊙) and    has_identity(D, ⊙) and    unary_operator(D, N) and    reflexive(D, ≈) and    symmetric(D, ≈) and    forall(a, i: D(a) and identity[D, ⊙](i) implies ((a ⊙ N[a]) ≈ i) and ((N[a] ⊙ a) ≈ i))

## left_zero#

left_zero[D, ⊙]


A left zero of a binary operator ⊙ is an element z such that z ⊙ a = z for all a in D.

#### Definition#

@inlinedef left_zero[D, ⊙] =    zero: D(zero) and    forall(a ∈ D: ((zero ⊙ a) = zero)) and    binary_operator(D, ⊙)

## has_left_zero#

has_left_zero(D, ⊙)


This returns true if ⊙ has a left zero.

#### Definition#

@inlinedef has_left_zero(D, ⊙) =    binary_operator(D, ⊙) and    exists(zero ∈ D: forall(a ∈ D: ((zero ⊙ a) = zero)))

## right_zero#

right_zero[D, ⊙]


A right zero of a binary operator ⊙ is an element z such that z ⊙ a = z for all a in D.

#### Definition#

@inlinedef right_zero[D, ⊙] =    zero: D(zero) and    forall(a ∈ D: ((a ⊙ zero) = zero)) and    binary_operator(D, ⊙)

## has_right_zero#

has_right_zero(D, ⊙)


This returns true if ⊙ has a right zero.

#### Definition#

@inlinedef has_right_zero(D, ⊙) =    binary_operator(D, ⊙) and    exists(zero ∈ D: forall(a ∈ D: ((a ⊙ zero) = zero)))

## approximately_left_distributive#

approximately_left_distributive(D, ⊗, ⊕, ≈)


A binary operator ⊗ is approximately left distributive over another binary operator ⊕ if a ⊗ (b ⊕ c) is approximately equal to (a ⊗ b) ⊕ (a ⊗ c) for all a, b and c in D.

#### Definition#

@inlinedef approximately_left_distributive(D, ⊗, ⊕, ≈) =    binary_operator(D, ⊗) and    binary_operator(D, ⊕) and    reflexive(D, ≈) and    symmetric(D, ≈) and    forall(a ∈ D, b ∈ D, c ∈ D: (a ⊗ (b ⊕ c)) ≈ ((a ⊗ b) ⊕ (a ⊗ c)))

## left_distributive#

left_distributive(D, ⊗, ⊕)


A binary operator ⊗ is left distributive over another binary operator ⊕ if a ⊗ (b ⊕ c) is equal to (a ⊗ b) ⊕ (a ⊗ c) for all a, b and c in D.

#### Definition#

@inlinedef left_distributive(D, ⊗, ⊕) =    approximately_left_distributive(D, ⊗, ⊕, =)

## approximately_right_distributive#

approximately_right_distributive(D, ⊗, ⊕, ≈)


A binary operator ⊗ is approximately right distributive over another binary operator ⊕ if (a ⊕ b) ⊗ c is approximately equal to (a ⊗ c) ⊕ (b ⊗ c) for all a, b and c in D.

#### Definition#

@inlinedef approximately_right_distributive(D, ⊗, ⊕, ≈) =    binary_operator(D, ⊗) and    binary_operator(D, ⊕) and    reflexive(D, ≈) and    symmetric(D, ≈) and    forall(a ∈ D, b ∈ D, c ∈ D: ((a ⊕ b) ⊗ c) ≈ ((a ⊗ c) ⊕ (b ⊗ c)))

## right_distributive#

right_distributive(D, ⊗, ⊕, ≈)


A binary operator ⊗ is right distributive over another binary operator ⊕ if (a ⊕ b) ⊗ c is equal to (a ⊗ c) ⊕ (b ⊗ c) for all a, b and c in D.

#### Definition#

@inlinedef right_distributive(D, ⊗, ⊕) =    approximately_right_distributive(D, ⊗, ⊕, =)

## approximately_distributive#

approximately_distributive(D, ⊗, ⊕, ≈)


A binary operator ⊗ is approximately distributive over another binary operator ⊕ if it is approximately both left and right distributive.

#### Definition#

@inlinedef approximately_distributive(D, ⊗, ⊕, ≈) =    approximately_left_distributive(D, ⊗, ⊕, ≈) and    approximately_right_distributive(D, ⊗, ⊕, ≈)

## distributive#

distributive(D, ⊗, ⊕)


A binary operator ⊗ is distributive over another binary operator ⊕ if it is both left and right distributive.

#### Definition#

@inlinedef distributive(D, ⊗, ⊕) =    approximately_distributive(D, ⊗, ⊕, =)

## absorption_laws#

absorption_laws(D, ⊓, ⊔)


Binary operator ⊓ and ⊔ obey absorption laws if a ⊔ (a ⊓ b) = a = a ⊓ (a ⊔ b) for all a and b in D. The absorption laws are one of the defining characteristics of the meet and join operations of a lattice.

#### Definition#

@inlinedef absorption_laws(D, ⊓, ⊔) =    binary_operator(D, ⊓) and    binary_operator(D, ⊔) and    forall(a ∈ D, b ∈ D: (a ⊔ (a ⊓ b)) = a = (a ⊓ (a ⊔ b)))

## approximately_zero_annihilation#

approximately_zero_annihilation(D, ⊙, ≈)


A binary relation ⊙ obeys approximate zero annihilation if there exists an element that is approximately both a left and right zero.

#### Definition#

@inlinedef approximately_zero_annihilation(D, ⊙, ≈) =    binary_operator(D, ⊙) and    reflexive(D, ≈) and    symmetric(D, ≈) and    exists(zero ∈ D: forall(a ∈ D: ((a ⊙ zero) ≈ zero) and ((zero ⊙ a) ≈ zero)))

## zero_of_operator#

zero_of_operator[D, ⊙]


A zero of a binary operator ⊙ is an element that is both a left and right zero.

#### Definition#

@inlinedef zero_of_operator[D, ⊙] =    zero: D(zero) and    left_zero[D, ⊙](zero) and    right_zero[D, ⊙](zero)

## zero_annihilation#

zero_annihilation(D, ⊙)


A binary relation ⊙ obeys zero annihilation if there exists an element that is both a left and right zero.

#### Definition#

@inlinedef zero_annihilation(D, ⊙) =    approximately_zero_annihilation(D, ⊙, =)

## semilattice#

semilattice(D, ⊓)


A semilattice is a set D, with an operator ⊓, such that ⊓ is commutative, associative, and idempotent. The classic example of a semilattice is a set of subsets with the intersection operator.

#### Definition#

@inlinedef semilattice(D, ⊓) =    commutative(D, ⊓) and    associative(D, ⊓) and    idempotent(D, ⊓)

## bounded_semilattice#

bounded_semilattice(D, ⊓)


A bounded semilattice is a semilattice with a maximal element. Equivalently, a semilattice is bounded if it is an idempotent commutative monoid.

#### Definition#

@inlinedef bounded_semilattice(D, ⊓) =    semilattice(D, ⊓) and    commutative_monoid(D, ⊓) and    has_identity(D, ⊓)

## lattice#

lattice(D, ⊓, ⊔)


A lattice is a set D with two operators, ⊓ and ⊔, usually denoted join and meet respectively, such that (D, ⊓) and (D, ⊔) are semilattices, and the operators ⊓ and ⊔ obey absorption laws.

#### Definition#

@inlinedef lattice(D, ⊓, ⊔) =    semilattice(D, ⊓) and    semilattice(D, ⊔) and    absorption_laws(D, ⊓, ⊔)

## meet_bounded_lattice#

meet_bounded_lattice(D, ⊓, ⊔)


A lattice is meet bounded if the meet operator ⊓ forms a bounded semilattice.

#### Definition#

@inlinedef meet_bounded_lattice(D, ⊓, ⊔) =    lattice(D, ⊓, ⊔) and    bounded_semilattice(D, ⊓)

## join_bounded_lattice#

join_bounded_lattice(D, ⊓, ⊔)


A lattice is join bounded if the join operator ⊔ forms a bounded semilattice.

#### Definition#

@inlinedef join_bounded_lattice(D, ⊓, ⊔) =    lattice(D, ⊓, ⊔) and    bounded_semilattice(D, ⊔)

## bounded_lattice#

bounded_lattice(D, ⊓, ⊔)


A lattice is bounded if both the meet and join operators form bounded semilattices.

#### Definition#

@inlinedef bounded_lattice(D, ⊓, ⊔) =    meet_bounded_lattice(D, ⊓, ⊔) and    join_bounded_lattice(D, ⊓, ⊔)

## partial_order_and_lattice#

partial_order_and_lattice(D, ≼, ⊓, ⊔)


A lattice is partially ordered if it has an operator ≼ defining a partial order, such that a ≼ b if and only if (a ⊓ b) = a, and (a ⊔ b) = b.

#### Definition#

@inlinedef partial_order_and_lattice(D, ≼, ⊓, ⊔) =    partial_order(D, ≼) and    lattice(D, ⊓, ⊔) and    forall(a ∈ D, b ∈ D: (a ≼ b) ≡ ((a ⊓ b) = a)) and    forall(a ∈ D, b ∈ D: (a ≼ b) ≡ ((a ⊔ b) = b))

## partial_order_and_meet_bounded_lattice#

partial_order_and_meet_bounded_lattice(D, ≼, ⊓, ⊔)


A partially ordered lattice is meet bounded if the meet operator ⊓ forms a bounded semilattice, and the identity of ⊓ is the maximal element of ≼.

#### Definition#

@inlinedef partial_order_and_meet_bounded_lattice(D, ≼, ⊓, ⊔) =    partial_order_and_lattice(D, ≼, ⊓, ⊔) and    meet_bounded_lattice(D, ⊓, ⊔) and    has_minimal_element(D, ≼) and    identity[D, ⊓] ≡ maximal_element[D, ≼]

## partial_order_and_join_bounded_lattice#

partial_order_and_join_bounded_lattice(D, ≼, ⊓, ⊔)


A partially ordered lattice is join bounded if the join operator ⊔ forms a bounded semilattice, and the identity of ⊔ is the minimal element of ≼.

#### Definition#

@inlinedef partial_order_and_join_bounded_lattice(D, ≼, ⊓, ⊔) =    partial_order_and_lattice(D, ≼, ⊓, ⊔) and    join_bounded_lattice(D, ⊓, ⊔) and    has_maximal_element(D, ≼) and    identity[D, ⊔] ≡ minimal_element[D, ≼]

## partial_order_and_bounded_lattice#

partial_order_and_bounded_lattice(D, ≼, ⊓, ⊔)


A partially ordered lattice is bounded if is both meet and join bounded.

#### Definition#

@inlinedef partial_order_and_bounded_lattice(D, ≼, ⊓, ⊔) =    partial_order_and_meet_bounded_lattice(D, ≼, ⊓, ⊔) and    partial_order_and_join_bounded_lattice(D, ≼, ⊓, ⊔)

## approximate_monoid#

approximate_monoid(D, ⊙, ≈)


An approximate monoid is a set D with a binary operator ⊙ that is approximately associative and has an identity element.

#### Definition#

@inlinedef approximate_monoid(D, ⊙, ≈) =    approximately_associative(D, ⊙, ≈) and    has_identity(D, ⊙)

## monoid#

monoid(D, ⊙)


A monoid is a set D with a binary operator ⊙ that is associative and has an identity element.

#### Definition#

@inlinedef monoid(D, ⊙) =    approximate_monoid(D, ⊙, =) and    associative(D, ⊙)

## approximate_commutative_monoid#

approximate_commutative_monoid(D, ⊙, ≈)


An approximate commutative monoid is an approximate monoid where the operator ⊙ is approximately commutative.

#### Definition#

@inlinedef approximate_commutative_monoid(D, ⊙, ≈) =    approximate_monoid(D, ⊙, ≈) and    approximately_commutative(D, ⊙, ≈)

## commutative_monoid#

commutative_monoid(D, ⊙)


A commutative monoid is a monoid where the operator ⊙ is commutative.

#### Definition#

@inlinedef commutative_monoid(D, ⊙) =    approximate_commutative_monoid(D, ⊙, =) and    commutative(D, ⊙)

## approximate_group#

approximate_group(D, ⊙, N, ≈)


An approximate group is an approximate monoid where the operator ⊙ has approximate inverses defined by N.

#### Definition#

@inlinedef approximate_group(D, ⊙, N, ≈) =    approximate_monoid(D, ⊙, ≈) and    approximately_has_inverse(D, ⊙, N, ≈)

## group#

group(D, ⊙, N)


A group is a monoid where the operator ⊙ has inverses defined by N.

#### Definition#

@inlinedef group(D, ⊙, N) =    approximate_group(D, ⊙, N, =) and    monoid(D, ⊙) and    approximately_has_inverse(D, ⊙, N, =)

## approximate_abelian_group#

approximate_abelian_group(D, ⊙, N, ≈)


An approximate abelian group is an approximate commutative monoid where the operator ⊙ has approximate inverses defined by N.

#### Definition#

@inlinedef approximate_abelian_group(D, ⊙, N, ≈) =    approximate_group(D, ⊙, N, ≈) and    approximate_commutative_monoid(D, ⊙, ≈)

## abelian_group#

abelian_group(D, ⊙, N)


An abelian group is a commutative monoid where the operator ⊙ has inverses defined by N.

#### Definition#

@inlinedef abelian_group(D, ⊙, N) =    approximate_abelian_group(D, ⊙, N, =) and    group(D, ⊙, N) and    commutative_monoid(D, ⊙)

## approximate_semiring#

approximate_semiring(D, ⊕, ⊙, ≈)


An approximate semiring is a set D with two operators, ⊕ and ⊙, where ⊕ forms an approximate commutative monoid, ⊙ forms an approximate monoid and has an approximate zero, ⊙ distributes over ⊕, and the identity of ⊕ is approximately equal to the zero of ⊙.

#### Definition#

@inlinedef approximate_semiring(D, ⊕, ⊙, ≈) =    approximate_commutative_monoid(D, ⊕, ≈) and    approximate_monoid(D, ⊙, ≈) and    approximately_distributive(D, ⊙, ⊕, ≈) and    approximately_zero_annihilation(D, ⊙, ≈) and    exists(x, y: zero_of_operator[D, ⊙](x) and identity[D, ⊕](y) implies x ≈ y)

## semiring#

semiring(D, ⊕, ⊙)


A semiring is an approximate semiring with equality defined as =.

#### Definition#

@inlinedef semiring(D, ⊕, ⊙) =    approximate_semiring(D, ⊕, ⊙, =) and    commutative_monoid(D, ⊕) and    monoid(D, ⊙) and    distributive(D, ⊙, ⊕) and    zero_annihilation(D, ⊙) and    zero_of_operator[D, ⊙] ≡ identity[D, ⊕]

## approximate_ring#

approximate_ring(D, ⊕, N, ⊙, ≈)


An approximate ring is an approximate semiring where the ⊕ operator has inverses defined by N.

#### Definition#

@inlinedef approximate_ring(D, ⊕, N, ⊙, ≈) =    approximate_abelian_group(D, ⊕, N, ≈) and    approximate_semiring(D, ⊕, ⊙, ≈)

## ring#

ring(D, ⊕, N, ⊙)


A ring is a semiring where the ⊕ operator has inverses.

#### Definition#

@inlinedef ring(D, ⊕, N, ⊙) =    approximate_ring(D, ⊕, N, ⊙, =) and    abelian_group(D, ⊕, N) and    semiring(D, ⊕, ⊙)