Skip to content
  • REL
  • REFERENCE
  • Libraries
  • alglib

The Algebra Library (alglib)

Collection of algebraic operations.

abelian_group

abelian_group(D, ⊙, N)

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

Definition

@inline
def abelian_group(D, ⊙, N) =
    approximate_abelian_group(D, ⊙, N, =) and
    group(D, ⊙, N) and
    commutative_monoid(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

@inline
def absorption_laws(D, ⊓, ⊔) =
    binary_operator(D, ⊓) and
    binary_operator(D, ⊔) and
    forall(a  D, b  D: (a ⊔ (a ⊓ b)) = a = (a ⊓ (a ⊔ b)))

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

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

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

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

approximate_commutative_monoid

approximate_commutative_monoid(D, ⊙, ≈)

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

Definition

@inline
def approximate_commutative_monoid(D, ⊙, ≈) =
    approximate_monoid(D, ⊙, ≈) and
    approximately_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

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

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

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

approximate_ring

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

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

Definition

@inline
def approximate_ring(D, ⊕, N, ⊙, ≈) =
    approximate_abelian_group(D, ⊕, N, ≈) and
    approximate_semiring(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

@inline
def 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)

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

@inline
def 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)))

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

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

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

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

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

@inline
def 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))

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

@inline
def 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)))

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

@inline
def 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)))

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

@inline
def 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)))

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

@inline
def associative(D, ⊙) =
    approximately_associative(D, ⊙, =)

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

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

binary_relation

binary_relation(∼)

true if is a binary relation.

Note: In case of is a operator, use space after as temporary workaround. eg., binary_relation(= )

Definition

@inline
def binary_relation( ∼ ) = equal(arity[∼], 2)

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

@inline
def binary_relation_substitution_laws(D, ∼, ≈) =
    binary_relation(∼ ) and binary_relation(≈ ) 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))

bounded_lattice

bounded_lattice(D, ⊓, ⊔)

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

Definition

@inline
def bounded_lattice(D, ⊓, ⊔) =
    meet_bounded_lattice(D, ⊓, ⊔) and
    join_bounded_lattice(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

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

commutative

commutative(D, ⊙)

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

Definition

@inline
def commutative(D, ⊙) =
    approximately_commutative(D, ⊙, =)

commutative_monoid

commutative_monoid(D, ⊙)

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

Definition

@inline
def commutative_monoid(D, ⊙) =
    approximate_commutative_monoid(D, ⊙, =) and
    commutative(D, ⊙)

comparable

comparable(a, b, ≼)

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

Definition

@inline
def comparable(a, b, ≼) =
    (a ≼ b) ∨ (b ≼ a)

distributive

distributive(D, ⊗, ⊕)

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

Definition

@inline
def distributive(D, ⊗, ⊕) =
    approximately_distributive(D, ⊗, ⊕, =)

equivalence_relation

equivalence_relation(D, ∼)

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

Definition

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

group

group(D, ⊙, N)

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

Definition

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

has_identity

has_identity(D, ⊙)

true if has an identity.

Definition

@inline
def has_identity(D, ⊙) =
    binary_operator(D, ⊙) and
    exists(ident  D: forall(a  D: (a ⊙ ident) = a and (ident ⊙ a) = a))

has_left_identity

has_left_identity(D, ⊙)

true if has a left identity.

Definition

@inline
def 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)))

has_left_zero

has_left_zero(D, ⊙)

true if has a left zero.

Definition

@inline
def has_left_zero(D, ⊙) =
    binary_operator(D, ⊙) and
    exists(zero  D: forall(a  D: ((zero ⊙ a) = zero)))

has_maximal_element

has_maximal_element(D, ≼)

true if the partial order contains a maximal element.

Definition

@inline
def has_maximal_element(D, ≼) =
    partial_order(D, ≼) and
    exists(max_elem  D: forall(a  D: a ≼ max_elem))

has_minimal_element

has_minimal_element(D, ≼)

true if the partial order contains a minimal element.

Definition

@inline
def has_minimal_element(D, ≼) =
    partial_order(D, ≼) and
    exists(min_elem  D: forall(a  D: min_elem ≼ a))

has_right_identity

has_right_identity(D, ⊙)

true if has a right identity.

Definition

@inline
def has_right_identity(D, ⊙) =
    binary_operator(D, ⊙) and
    exists(ident  D: forall(a  D: ((a ⊙ ident) = a)))

has_right_zero

has_right_zero(D, ⊙)

true if has a right zero.

Definition

@inline
def has_right_zero(D, ⊙) =
    binary_operator(D, ⊙) and
    exists(zero  D: forall(a  D: ((a ⊙ zero) = zero)))

idempotent

idempotent(D, ⊙, ≈)

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

Definition

@inline
def idempotent(D, ⊙) =
    binary_operator(D, ⊙) and
    forall(a  D: (a ⊙ a) = a)

identity

identity[D, ⊙]

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

Definition

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

irreflexive

irreflexive(D, ∼)

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

Definition

@inline
def irreflexive(D, ∼) =
    binary_relation(∼ ) and
    forall(a  D: ¬(a ∼ a))

join_bounded_lattice

join_bounded_lattice(D, ⊓, ⊔)

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

Definition

@inline
def join_bounded_lattice(D, ⊓, ⊔) =
    lattice(D, ⊓, ⊔) and
    bounded_semilattice(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

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

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

@inline
def left_distributive(D, ⊗, ⊕) =
    approximately_left_distributive(D, ⊗, ⊕, =)

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

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

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

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

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

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

meet_bounded_lattice

meet_bounded_lattice(D, ⊓, ⊔)

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

Definition

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

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

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

monoid

monoid(D, ⊙)

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

Definition

@inline
def monoid(D, ⊙) =
    approximate_monoid(D, ⊙, =) and
    associative(D, ⊙)

nullary_relation

nullary_relation(∼)

true if is a relation of 0-arity.

Note: In case of is a operator, use space after as temporary workaround. eg., nullary_relation(= )

Definition

@inline
def nullary_relation( ∼ ) = equal(arity[∼], 0)

partial_order

partial_order(D, ≼)

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

Definition

@inline
def partial_order(D, ≼) =
    reflexive(D, ≼) and antisymmetric(D, ≼) and transitive(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

@inline
def partial_order_and_bounded_lattice(D, ≼, ⊓, ⊔) =
    partial_order_and_meet_bounded_lattice(D, ≼, ⊓, ⊔) and
    partial_order_and_join_bounded_lattice(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

@inline
def partial_order_and_join_bounded_lattice(D, ≼, ⊓, ⊔) =
    partial_order_and_lattice(D, ≼, ⊓, ⊔) and
    join_bounded_lattice(D, ⊓, ⊔) and
    has_maximal_element(D, ≼) and
    equal(identity[D, ⊔], minimal_element[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

@inline
def 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

@inline
def partial_order_and_meet_bounded_lattice(D, ≼, ⊓, ⊔) =
    partial_order_and_lattice(D, ≼, ⊓, ⊔) and
    meet_bounded_lattice(D, ⊓, ⊔) and
    has_minimal_element(D, ≼) and
    equal(identity[D, ⊓], maximal_element[D, ≼])

preorder

preorder(D, ≼)

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

Definition

@inline
def preorder(D, ≼) =
    reflexive(D, ≼) and transitive(D, ≼)

reflexive

reflexive(D, ∼)

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

Definition

@inline
def reflexive(D, ∼) =
    binary_relation(∼ ) and
    forall(a  D: a ∼ a)

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

@inline
def right_distributive(D, ⊗, ⊕) =
    approximately_right_distributive(D, ⊗, ⊕, =)

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

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

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

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

ring

ring(D, ⊕, N, ⊙)

A ring is a semiring where the operator has inverses.

Definition

@inline
def ring(D, ⊕, N, ⊙) =
    approximate_ring(D, ⊕, N, ⊙, =) and
    abelian_group(D, ⊕, N) and
    semiring(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

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

semiring

semiring(D, ⊕, ⊙)

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

Definition

@inline
def semiring(D, ⊕, ⊙) =
    approximate_semiring(D, ⊕, ⊙, =) and
    commutative_monoid(D, ⊕) and
    monoid(D, ⊙) and
    distributive(D, ⊙, ⊕) and
    zero_annihilation(D, ⊙) and
    equal(zero_of_operator[D, ⊙], identity[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

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

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

@inline
def strict_total_order(D, ≺) =
    strict_partial_order(D, ≺) and
    forall(a  D, b  D: comparable(a, b, ≺) ∨ (b = 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

@inline
def symmetric(D, ∼) =
    binary_relation(∼ ) and
    forall(a  D, b  D: a ∼ b ≡ b ∼ a)

ternary_relation

ternary_relation(∼)

true if is a ternary relation.

Note: In case of is a operator, use space after as temporary workaround. eg., ternary_relation(= )

Definition

@inline
def ternary_relation( ∼ ) = equal(arity[∼], 3)

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

@inline
def total_order(D, ≼) =
    partial_order(D, ≼) and
    forall(a  D, b  D: comparable(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

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

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

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

unary_relation

unary_relation(∼)

true if is a unary relation.

Note: In case of is a operator, use space after as temporary workaround. eg., unary_relation(= )

Definition

@inline
def unary_relation( ∼ ) = equal(arity[∼], 1)

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

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

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

@inline
def zero_annihilation(D, ⊙) =
    approximately_zero_annihilation(D, ⊙, =)

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

@inline
def zero_of_operator[D, ⊙] =
    zero: D(zero) and
    left_zero[D, ⊙](zero) and
    right_zero[D, ⊙](zero)
Was this doc helpful?