OpenMath Content Dictionary: algebraic_cats

Canonical URL:
http://www.openmath.org/cd/algebraic_cats.ocd
CD File:
algebraic_cats.ocd
CD as XML Encoded OpenMath:
algebraic_cats.omcd
Defines:
Abelian_group, Abelian_group_identity, Abelian_group_inverse, Abelian_group_operation, Abelian_group_set, Abelian_monoid, Abelian_monoid_identity, Abelian_monoid_operation, Abelian_monoid_set, Abelian_semigroup, Abelian_semigroup_operation, Abelian_semigroup_set, Euclidean_domain, Euclidean_domain_abs, Euclidean_domain_negative, Euclidean_domain_plus, Euclidean_domain_set, Euclidean_domain_times, Euclidean_domain_zero, field, field_negative, field_one, field_plus, field_reciprocal, field_set, field_times, field_zero, group, group_identity, group_inverse, group_operation, group_set, groupoid, groupoid_operation, groupoid_set, integral_domain, integral_domain_negative, integral_domain_one, integral_domain_plus, integral_domain_set, integral_domain_times, integral_domain_zero, monoid, monoid_identity, monoid_operation, monoid_set, non_commutative_ring, non_commutative_ring_negative, non_commutative_ring_plus, non_commutative_ring_set, non_commutative_ring_times, non_commutative_ring_zero, ordered_Abelian_group, ordered_Abelian_group_identity, ordered_Abelian_group_inverse, ordered_Abelian_group_operation, ordered_Abelian_group_order, ordered_Abelian_group_set, ordered_Abelian_monoid, ordered_Abelian_monoid_identity, ordered_Abelian_monoid_operation, ordered_Abelian_monoid_order, ordered_Abelian_monoid_set, ordered_group, ordered_group_identity, ordered_group_inverse, ordered_group_operation, ordered_group_order, ordered_group_set, ordered_monoid, ordered_monoid_identity, ordered_monoid_operation, ordered_monoid_order, ordered_monoid_set, ordered_ring, ordered_ring_negative, ordered_ring_order, ordered_ring_plus, ordered_ring_set, ordered_ring_times, ordered_ring_zero, ring, ring_negative, ring_plus, ring_set, ring_times, ring_zero, ringoid, ringoid_plus, ringoid_set, ringoid_times, semigroup, semigroup_operation, semigroup_set
Date:
2002-06-17
Version:
0 (Revision 3)
Review Date:
2017-12-31
Status:
experimental


     This document is distributed in the hope that it will be useful, 
     but WITHOUT ANY WARRANTY; without even the implied warranty of 
     MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.

     The copyright holder grants you permission to redistribute this 
     document freely as a verbatim copy. Furthermore, the copyright
     holder permits you to develop any derived work from this document
     provided that the following conditions are met.
       a) The derived work acknowledges the fact that it is derived from
          this document, and maintains a prominent reference in the 
          work to the original source.
       b) The fact that the derived work is not the original OpenMath 
          document is stated prominently in the derived work.  Moreover if
          both this document and the derived work are Content Dictionaries
          then the derived work must include a different CDName element,
          chosen so that it cannot be confused with any works adopted by
          the OpenMath Society.  In particular, if there is a Content 
          Dictionary Group whose name is, for example, `math' containing
          Content Dictionaries named `math1', `math2' etc., then you should 
          not name a derived Content Dictionary `mathN' where N is an integer.
          However you are free to name it `private_mathN' or some such.  This
          is because the names `mathN' may be used by the OpenMath Society
          for future extensions.
       c) The derived work is distributed under terms that allow the
          compilation of derived works, but keep paragraphs a) and b)
          intact.  The simplest way to do this is to distribute the derived
          work under the OpenMath license, but this is not a requirement.
     If you have questions about this license please contact the OpenMath
     society at http://www.openmath.org.
  Author: J B Collins
  Author: Bill Naylor

A CD of basic algebraic category constructors. This CD holds constructors of individual instances of the categories, with defining properties of the categories and accessor symbols to allow access to attributes of the categories.


monoid

Description:

This is the constructor for monoids. A monoid comprises a set and an operation over elements of the set. The set must contain a unique identity element (relative to the operation). That is an element, I, such that I*a=a*I=a where a represents an arbitrary element of S and * represents the operation. The operation * must be associative over S. The monoid constructor takes three arguments, the set of the monoid, a binary function taking two elements of the set into itself to represent the operation of the monoid and an element of the set to represent the identity of the monoid.

Commented Mathematical property (CMP):
This constructor may be used to build monoids
Formal Mathematical property (FMP):
monoid ( S , star ) monoid
Commented Mathematical property (CMP):
if (S,*,1) comprises a monoid then for all a,b,c in S | a*(b*c)=(a*b)*c
Formal Mathematical property (FMP):
S monoid a , b , c . a monoid_set ( S ) b monoid_set ( S ) c monoid_set ( S ) ( monoid_operation ( S ) ) ( a , ( monoid_operation ( S ) ) ( b , c ) ) = ( monoid_operation ( S ) ) ( ( monoid_operation ( S ) ) ( a , b ) , c )
Commented Mathematical property (CMP):
the operation of the monoid is closed over the set of the monoid
Formal Mathematical property (FMP):
S monoid a monoid_set ( S ) b monoid_set ( S ) ( monoid_operation ( S ) ) ( a , b ) monoid_set ( S )
Commented Mathematical property (CMP):
if (S,*,1) is a monoid then there exists a unique identity element in S
Formal Mathematical property (FMP):
S monoid id . x . ( monoid_operation ( S ) ) ( x , id ) = x id = monoid_identity ( S ) ( ( monoid_operation ( S ) ) ( x , id 2 ) = x id = id 2 )
Commented Mathematical property (CMP):
the set of a monoid must contain at least one element
Formal Mathematical property (FMP):
S monoid x . x monoid_set ( S )
Signatures:
sts


[Next: monoid_set] [Last: integral_domain_negative] [Top]

monoid_set

Description:

This symbol takes one argument which should be a monoid, it returns the set of the monoid.

Commented Mathematical property (CMP):
The set of the monoid (S,*,1) = S
Formal Mathematical property (FMP):
monoid_set ( monoid ( S , star , id ) ) = S
Signatures:
sts


[Next: monoid_operation] [Previous: monoid] [Top]

monoid_operation

Description:

This symbol takes one argument which should be a monoid, it returns the operation of the monoid.

Commented Mathematical property (CMP):
The operation of the monoid (S,*,1) = *
Formal Mathematical property (FMP):
monoid_operation ( monoid ( S , star , id ) ) = star
Signatures:
sts


[Next: monoid_identity] [Previous: monoid_set] [Top]

monoid_identity

Description:

This symbol takes one argument which should be a monoid, it returns the identity of the monoid.

Commented Mathematical property (CMP):
The identity of the monoid (S,*,1) = 1
Formal Mathematical property (FMP):
monoid_identity ( monoid ( S , star , id ) ) = id
Signatures:
sts


[Next: Abelian_monoid] [Previous: monoid_operation] [Top]

Abelian_monoid

Description:

This is the constructor for Abelian monoids. An Abelian monoid is a monoid, such that the operation is commutative between members of the Abelian monoid. The Abelian_monoid constructor takes three arguments, the set of the Abelian monoid, a binary function taking two elements of the set into itself to represent the operation of the Abelian monoid and an element of the set to represent the identity of the Abelian monoid.

Commented Mathematical property (CMP):
This constructor may be used to build Abelian_monoids
Formal Mathematical property (FMP):
Abelian_monoid ( S , star , Id ) Abelian_monoid
Commented Mathematical property (CMP):
if (S,*,1) comprises an Abelian monoid then for all a,b in S | a*b=b*a
Formal Mathematical property (FMP):
S Abelian_monoid a , b . a Abelian_monoid ( S ) b Abelian_monoid ( S ) ( Abelian_monoid_operation ( S ) ) ( a , b ) = ( Abelian_monoid_operation ( S ) ) ( b , a )
Signatures:
sts


[Next: Abelian_monoid_set] [Previous: monoid_identity] [Top]

Abelian_monoid_set

Description:

This symbol takes one argument which should be an Abelian monoid, it returns the set of the Abelian monoid.

Commented Mathematical property (CMP):
The set of the Abelian monoid (S,*,1) = S
Formal Mathematical property (FMP):
Abelian_monoid_set ( Abelian_monoid ( S , star , id ) ) = S
Signatures:
sts


[Next: Abelian_monoid_operation] [Previous: Abelian_monoid] [Top]

Abelian_monoid_operation

Description:

This symbol takes one argument which should be an Abelian monoid, it returns the operation of the Abelian monoid.

Commented Mathematical property (CMP):
The operation of the Abelian monoid (S,*,1)= *
Formal Mathematical property (FMP):
Abelian_monoid_set ( Abelian_monoid ( S , star , id ) ) = star
Signatures:
sts


[Next: Abelian_monoid_identity] [Previous: Abelian_monoid_set] [Top]

Abelian_monoid_identity

Description:

This symbol takes one argument which should be an Abelian monoid, it returns the identity of the Abelian monoid.

Commented Mathematical property (CMP):
The identity of the Abelian monoid (S,*,1) = 1
Formal Mathematical property (FMP):
Abelian_monoid_set ( Abelian_monoid ( S , star , id ) ) = id
Signatures:
sts


[Next: ordered_monoid] [Previous: Abelian_monoid_operation] [Top]

ordered_monoid

Description:

This is the constructor for ordered monoids, that is monoids on which there is an ordering relation. The ordered_monoid constructor takes four arguments, the set of the ordered monoid, a binary function taking two elements of the set into itself to represent the operation of the ordered monoid, an element of the set to represent the identity of the ordered monoid and a binary function taking two elements of the set into the booleans to represent the ordering on the ordered monoid.

Commented Mathematical property (CMP):
This constructor may be used to build ordered monoids
Formal Mathematical property (FMP):
ordered_monoid ( S , star , Id , lt ) ordered_monoid
Commented Mathematical property (CMP):
if (S,*,1,\leq) represents an ordered monoid, then for all a,b in S | a \leq b or b \leq a and for all a,b,c in S | if a\leq b and b\leq c then a\leq c and for all a,b in S | if a\leq b and b\leq a then a=b
Formal Mathematical property (FMP):
S ordered_monoid a , b . a ordered_monoid_set ( S ) b ordered_monoid_set ( S ) ( ordered_monoid_order ( S ) ) ( a , b ) ( ordered_monoid_order ( S ) ) ( b , a ) a , b , c . a ordered_monoid_set ( S ) b ordered_monoid_set ( S ) c ordered_monoid_set ( S ) ( ordered_monoid_order ( S ) ) ( a , b ) ( ordered_monoid_order ( S ) ) ( b , c ) ( ordered_monoid_order ( S ) ) ( a , c ) a , b . a ordered_monoid_set ( S ) b ordered_monoid_set ( S ) ( ordered_monoid_order ( S ) ) ( a , b ) ( ordered_monoid_order ( S ) ) ( b , a ) a = b
Signatures:
sts


[Next: ordered_monoid_set] [Previous: Abelian_monoid_identity] [Top]

ordered_monoid_set

Description:

This symbol takes one argument which should be an ordered monoid. It returns a set which should be the set of the ordered monoid.

Commented Mathematical property (CMP):
The set of the ordered monoid (S,*,1,\leq) = S
Formal Mathematical property (FMP):
ordered_monoid_set ( ordered_monoid ( S , star , id , leq ) ) = S
Signatures:
sts


[Next: ordered_monoid_operation] [Previous: ordered_monoid] [Top]

ordered_monoid_operation

Description:

This symbol takes one argument which should be an ordered monoid. It returns a binary function between elements of the set of the ordered monoid, which should represent the operation of the ordered monoid.

Commented Mathematical property (CMP):
The operation of the ordered monoid (S,*,1,\leq) = *
Formal Mathematical property (FMP):
ordered_monoid_operation ( ordered_monoid ( S , star , id , leq ) ) = star
Signatures:
sts


[Next: ordered_monoid_identity] [Previous: ordered_monoid_set] [Top]

ordered_monoid_identity

Description:

This symbol takes one argument which should be an ordered monoid. It returns an element of the set of the ordered monoid, which should be the identity of the ordered monoid.

Commented Mathematical property (CMP):
The identity of the ordered monoid (S,*,1,\leq) = 1
Formal Mathematical property (FMP):
ordered_monoid_identity ( ordered_monoid ( S , star , id , leq ) ) = id
Signatures:
sts


[Next: ordered_monoid_order] [Previous: ordered_monoid_operation] [Top]

ordered_monoid_order

Description:

This symbol takes one argument which should be an ordered monoid. It returns a binary function between elements of the set of the ordered monoid, which should represent the ordering relation on the ordered monoid.

Commented Mathematical property (CMP):
The order of the ordered monoid (S,*,1,\leq) = \leq
Formal Mathematical property (FMP):
ordered_monoid_order ( ordered_monoid ( S , star , id , leq ) ) = leq
Signatures:
sts


[Next: ordered_Abelian_monoid] [Previous: ordered_monoid_identity] [Top]

ordered_Abelian_monoid

Description:

This symbol is the constructor for ordered Abelian monoids, that is Abelian monoids on which there is an ordering relation. The ordered_Abelian_monoid constructor takes four arguments, the set of the ordered Abelian monoid, a binary function taking two elements of the set into itself to represent the operation of the ordered Abelian monoid, an element of the set to represent the identity of the ordered Abelian monoid and a binary function taking two elements of the set into the booleans to represent the ordering of the ordered Abelian monoid.

Commented Mathematical property (CMP):
This constructor may be used to build ordered Abelian monoids
Formal Mathematical property (FMP):
ordered_Abelian_monoid ( S , star , Id , lt ) ordered_Abelian_monoid
Commented Mathematical property (CMP):
if (S,*,1,\leq) represents an ordered Abelian monoid, then for all a,b in S | a \leq b or b \leq a and for all a,b,c in S | if a\leq b and b\leq c then a\leq c and for all a,b in S | if a\leq b and b\leq a then a=b
Formal Mathematical property (FMP):
S ordered_Abelian_monoid a , b . a ordered_Abelian_monoid_set ( S ) b ordered_Abelian_monoid_set ( S ) ( ordered_monoid_order ( S ) ) ( a , b ) ( ordered_monoid_order ( S ) ) ( b , a ) a , b , c . a ordered_Abelian_monoid_set ( S ) b ordered_Abelian_monoid_set ( S ) c ordered_Abelian_monoid_set ( S ) ( ordered_Abelian_monoid_order ( S ) ) ( a , b ) ( ordered_Abelian_monoid_order ( S ) ) ( b , c ) ( ordered_Abelian_monoid_order ( S ) ) ( a , c ) a , b . a ordered_Abelian_monoid_set ( S ) b ordered_Abelian_monoid_set ( S ) ( ordered_Abelian_monoid_order ( S ) ) ( a , b ) ( ordered_Abelian_monoid_order ( S ) ) ( b , a ) a = b
Signatures:
sts


[Next: ordered_Abelian_monoid_set] [Previous: ordered_monoid_order] [Top]

ordered_Abelian_monoid_set

Description:

This symbol takes one argument which should be an ordered Abelian monoid. It returns a set which should be the set of the ordered Abelian monoid.

Commented Mathematical property (CMP):
The set of the ordered Abelian monoid (S,*,1,/leq) = S
Formal Mathematical property (FMP):
ordered_Abelian_monoid_set ( ordered_Abelian_monoid ( S , star , id , leq ) ) = S
Signatures:
sts


[Next: ordered_Abelian_monoid_operation] [Previous: ordered_Abelian_monoid] [Top]

ordered_Abelian_monoid_operation

Description:

This symbol takes one argument which should be an ordered Abelian monoid. It returns a binary function between elements of the set of the ordered Abelian monoid, which should represent the operation of the ordered Abelian monoid.

Commented Mathematical property (CMP):
The operation of the ordered Abelian monoid (S,*,1,/leq) = *
Formal Mathematical property (FMP):
ordered_Abelian_monoid_operation ( ordered_Abelian_monoid ( S , star , id , leq ) ) = star
Signatures:
sts


[Next: ordered_Abelian_monoid_identity] [Previous: ordered_Abelian_monoid_set] [Top]

ordered_Abelian_monoid_identity

Description:

This symbol takes one argument which should be an ordered Abelian monoid. It returns an element of the set of the ordered Abelian monoid, which should be the identity of the ordered Abelian monoid.

Commented Mathematical property (CMP):
The identity of the ordered Abelian monoid (S,*,1,/leq) = 1
Formal Mathematical property (FMP):
ordered_Abelian_monoid_identity ( ordered_Abelian_monoid ( S , star , id , leq ) ) = id
Signatures:
sts


[Next: ordered_Abelian_monoid_order] [Previous: ordered_Abelian_monoid_operation] [Top]

ordered_Abelian_monoid_order

Description:

This symbol takes one argument which should be an ordered Abelian monoid. It returns a binary function between elements of the set of the ordered Abelian monoid, which should represent the ordering relation on the ordered Abelian monoid.

Commented Mathematical property (CMP):
The ordering of the ordered Abelian monoid (S,*,1,/leq) = /leq
Formal Mathematical property (FMP):
ordered_Abelian_monoid_order ( ordered_Abelian_monoid ( S , star , id , leq ) ) = leq
Signatures:
sts


[Next: groupoid] [Previous: ordered_Abelian_monoid_identity] [Top]

groupoid

Description:

This symbol is the constructor for groupoids, that is an algebraic structure on a set, with a binary operation. The operator of the groupoid must be closed over the set of the groupoid. The groupoid constructor takes two arguments, the set of the groupoid and a binary function which represents the operation of the groupoid.

Commented Mathematical property (CMP):
This constructor may be used to build groupoids
Formal Mathematical property (FMP):
groupoid ( S , star ) groupoid
Commented Mathematical property (CMP):
if (S,*) comprises a groupoid, then for all a,b in S | a*b is a member of S
Formal Mathematical property (FMP):
S groupoid a , b . a groupoid_set ( S ) b groupoid_set ( S ) ( groupoid_operation ( S ) ) ( a , b ) groupoid_set ( S )
Signatures:
sts


[Next: groupoid_set] [Previous: ordered_Abelian_monoid_order] [Top]

groupoid_set

Description:

This symbol takes one argument which should be a groupoid. It returns the set of the groupoid.

Commented Mathematical property (CMP):
The set of the groupoid (S,*) = S
Formal Mathematical property (FMP):
groupoid_set ( groupoid ( S , star ) ) = S
Signatures:
sts


[Next: groupoid_operation] [Previous: groupoid] [Top]

groupoid_operation

Description:

This symbol takes one argument which should be a groupoid. It returns a binary function which should represent the operation of the groupoid.

Commented Mathematical property (CMP):
The operation of the groupoid (S,*) = *
Formal Mathematical property (FMP):
groupoid_operation ( groupoid ( S , star ) ) = star
Signatures:
sts


[Next: semigroup] [Previous: groupoid_set] [Top]

semigroup

Description:

This symbol is the constructor for semigroups, that is groupoids for which the operator of the semigroup is associative over the set of the semigroup. The semigroup constructor takes two arguments, the set of the semigroup and a binary function which represents the operation of the semigroup.

Commented Mathematical property (CMP):
This constructor may be used to build semigroups
Formal Mathematical property (FMP):
semigroup ( S , star ) semigroup
Commented Mathematical property (CMP):
if (S,*) comprises a semigroup then for all a,b,c in S | a*(b*c)=(a*b)*c
Signatures:
sts


[Next: semigroup_set] [Previous: groupoid_operation] [Top]

semigroup_set

Description:

This symbol takes one argument which should be a semigroup. It returns the set of the semigroup.

Commented Mathematical property (CMP):
The set of the semigroup (S,*) = S
Formal Mathematical property (FMP):
semigroup_set ( semigroup ( S , star ) ) = S
Signatures:
sts


[Next: semigroup_operation] [Previous: semigroup] [Top]

semigroup_operation

Description:

This symbol takes one argument which should be a semigroup. It returns a binary function which should represent the operation of the semigroup.

Commented Mathematical property (CMP):
The operation of the semigroup (S,*) = *
Formal Mathematical property (FMP):
semigroup_operation ( semigroup ( S , star ) ) = star
Signatures:
sts


[Next: Abelian_semigroup] [Previous: semigroup_set] [Top]

Abelian_semigroup

Description:

This symbol is the constructor for an Abelian semigroup, that is a semigroup which has an operator which is commutative over the set of the semigroup. The Abelian semigroup constructor takes two arguments, the set of the Abelian semigroup and a binary function which represents the operation of the Abelian semigroup.

Commented Mathematical property (CMP):
This constructor may be used to build Abelian semigroups
Formal Mathematical property (FMP):
Abelian_semigroup ( S , star ) Abelian_semigroup
Commented Mathematical property (CMP):
If (S,*) comprises an Abelian semigroup, then for all a,b in S|a*b=b*a
Formal Mathematical property (FMP):
S Abelian_semigroup a , b . a Abelian_semigroup ( S ) b Abelian_semigroup ( S ) ( Abelian_semigroup_operation ( S ) ) ( a , b ) = ( Abelian_semigroup_operation ( S ) ) ( b , a )
Signatures:
sts


[Next: Abelian_semigroup_set] [Previous: semigroup_operation] [Top]

Abelian_semigroup_set

Description:

This symbol takes one argument which should be an Abelian semigroup. It returns a set, which should be the set of the Abelian semigroup.

Commented Mathematical property (CMP):
The set of the Abelian semigroup (S,*) = S
Formal Mathematical property (FMP):
Abelian_semigroup_set ( Abelian_semigroup ( S , star ) ) = S
Signatures:
sts


[Next: Abelian_semigroup_operation] [Previous: Abelian_semigroup] [Top]

Abelian_semigroup_operation

Description:

This symbol takes one argument which should be an Abelian semigroup. It returns a binary function, which should represent the operation of the Abelian semigroup.

Commented Mathematical property (CMP):
The operation of the Abelian semigroup (S,*) = *
Formal Mathematical property (FMP):
Abelian_semigroup_operation ( Abelian_semigroup ( S , star ) ) = star
Signatures:
sts


[Next: group] [Previous: Abelian_semigroup_set] [Top]

This symbol is an alternative model for the symbol declare_group in
the CD group1

group

Description:

This symbol is the constructor for groups, that is a monoid for which every element is invertible. The group constructor takes four arguments, the set of the group, a binary function taking two elements of the set into itself to represent the operation of the group, an element of the set to represent the identity of the group and a unary function taking the set into itself to specify inverse elements of the group.

Commented Mathematical property (CMP):
This symbol may be used to build groups
Formal Mathematical property (FMP):
group ( S , star ) group
Commented Mathematical property (CMP):
if (S,*,1,inv:S->S) comprises a group then for all a in S | inv(a) is a member of S and inv(a)*a=a*inv(a)=1
Formal Mathematical property (FMP):
S group a . a group_set ( S ) in ( a , group_set ( S ) ) ( group_operation ( S ) ) ( group_inverse ( a ) , a ) = group_identity ( S ) ( group_operation ( S ) ) ( a , group_inverse ( a ) ) = group_identity ( S )
Signatures:
sts


[Next: group_set] [Previous: Abelian_semigroup_operation] [Top]

group_set

Description:

This symbol takes one argument which should be a group. It returns a set, which should be the set of the group.

Commented Mathematical property (CMP):
The set of the group (S,*,1,inv) = S
Formal Mathematical property (FMP):
group_set ( group ( S , star , id , inv ) ) = S
Signatures:
sts


[Next: group_operation] [Previous: group] [Top]

group_operation

Description:

This symbol takes one argument which should be a group. It returns a binary function, which represents the operation of the group.

Commented Mathematical property (CMP):
The operation of the group (S,*,1,inv) = *
Formal Mathematical property (FMP):
group_operation ( group ( S , star , id , inv ) ) = star
Signatures:
sts


[Next: group_identity] [Previous: group_set] [Top]

group_identity

Description:

This symbol takes one argument which should be a group. It returns the identity of the group.

Commented Mathematical property (CMP):
The identity of the group (S,*,1,inv) = 1
Formal Mathematical property (FMP):
group_identity ( group ( S , star , id , inv ) ) = id
Signatures:
sts


[Next: group_inverse] [Previous: group_operation] [Top]

group_inverse

Description:

This symbol takes one argument which should be a group. It returns a unary function, which is the inverse mapping for the group.

Commented Mathematical property (CMP):
The inverse of the group (S,*,1,inv) = inv
Formal Mathematical property (FMP):
group_inverse ( group ( S , star , id , inv ) ) = inv
Signatures:
sts


[Next: ordered_group] [Previous: group_identity] [Top]

ordered_group

Description:

This symbol is the constructor for ordered groups, that is a group on which there is an ordering relation. The ordered_group constructor takes five arguments, the set of the ordered group, a binary function taking two elements of the set into itself to represent the operation of the ordered group, an element of the set to represent the identity of the ordered group, a unary function taking the set into itself to specify inverse elements of the ordered group and a binary function taking two elements of the set into the booleans to specify the ordering of the ordered group.

Commented Mathematical property (CMP):
This constructor may be used to build ordered groups
Formal Mathematical property (FMP):
ordered_group ( S , star , id , inv , leq ) ordered_group
Commented Mathematical property (CMP):
if (S,*,1,inv:S->S,\leq) represents an ordered group, then for all a,b in S | a \leq b or b \leq a and for all a,b,c in S | if a\leq b and b\leq c then a\leq c and for all a,b in S | if a\leq b and b\leq a then a=b
Formal Mathematical property (FMP):
S ordered_group a , b . a ordered_group_set ( S ) b ordered_group_set ( S ) ( ordered_group_order ( S ) ) ( a , b ) ( ordered_group_order ( S ) ) ( b , a ) a , b , c . a ordered_group_set ( S ) b ordered_group_set ( S ) c ordered_group_set ( S ) ( ordered_group_order ( S ) ) ( a , b ) ( ordered_group_order ( S ) ) ( b , c ) ( ordered_group_order ( S ) ) ( a , c ) a , b . a ordered_group_set ( S ) b ordered_group_set ( S ) ( ordered_group_order ( S ) ) ( a , b ) ( ordered_group_order ( S ) ) ( b , a ) a = b
Signatures:
sts


[Next: ordered_group_set] [Previous: group_inverse] [Top]

ordered_group_set

Description:

This symbol takes one argument which should be an ordered group. It returns the set of the ordered group.

Commented Mathematical property (CMP):
The set of the ordered group (S,*,1,inv,leq) = S
Formal Mathematical property (FMP):
ordered_group_set ( ordered_group ( S , star , id , inv , leq ) ) = S
Signatures:
sts


[Next: ordered_group_operation] [Previous: ordered_group] [Top]

ordered_group_operation

Description:

This symbol takes one argument which should be an ordered group. It returns a binary function, which represents the operation of the ordered group.

Commented Mathematical property (CMP):
The operation of the ordered group (S,*,1,inv,leq) = *
Formal Mathematical property (FMP):
ordered_group_operation ( ordered_group ( S , star , id , inv , leq ) ) = missing
Signatures:
sts


[Next: ordered_group_identity] [Previous: ordered_group_set] [Top]

ordered_group_identity

Description:

This symbol takes one argument which should be an ordered group. It returns the identity of the ordered group.

Commented Mathematical property (CMP):
The identity of the ordered group (S,*,1,inv,leq) = 1
Formal Mathematical property (FMP):
ordered_group_identity ( ordered_group ( S , star , id , inv , leq ) ) = id
Signatures:
sts


[Next: ordered_group_inverse] [Previous: ordered_group_operation] [Top]

ordered_group_inverse

Description:

This symbol takes one argument which should be an ordered group. It returns a unary function, which is the inverse function of the ordered group.

Commented Mathematical property (CMP):
The inverse of the ordered group (S,*,1,inv,leq) = inv
Formal Mathematical property (FMP):
ordered_group_inverse ( ordered_group ( S , star , id , inv , leq ) ) = inv
Signatures:
sts


[Next: ordered_group_order] [Previous: ordered_group_identity] [Top]

ordered_group_order

Description:

This symbol takes one argument which should be an ordered group. It returns a binary function, which represents the ordering of the ordered group.

Commented Mathematical property (CMP):
The order of the ordered group (S,*,1,inv,leq) = leq
Formal Mathematical property (FMP):
ordered_group_order ( ordered_group ( S , star , id , inv , leq ) ) = leq
Signatures:
sts


[Next: Abelian_group] [Previous: ordered_group_inverse] [Top]

Abelian_group

Description:

This symbol is the constructor for Abelian groups, that is a group such that the operation is commutative between members of the group. The Abelian_group constructor takes four arguments, the set of the Abelian group, a binary function taking two elements of the set into itself to represent the operation of the Abelian group, an element of the set to represent the identity of the Abelian group and a unary function taking the set into itself to specify inverse elements.

Commented Mathematical property (CMP):
This constructor builds Abelian groups
Formal Mathematical property (FMP):
Abelian_group ( S , star , id , inv ) Abelian_group
Commented Mathematical property (CMP):
if (S,*,1,inv) comprises an Abelian group then for all a,b in S | a*b = b*a
Formal Mathematical property (FMP):
S Abelian_group a , b . a Abelian_group_set ( S ) b Abelian_group_set ( S ) ( Abelian_group_operation ( S ) ) ( a , b ) = ( Abelian_group_operation ( S ) ) ( b , a )
Signatures:
sts


[Next: Abelian_group_set] [Previous: ordered_group_order] [Top]

Abelian_group_set

Description:

This symbol takes one argument which should be an Abelian group. It returns the set of the Abelian group.

Commented Mathematical property (CMP):
The set of the Abelian group (S,*,1,inv) = S
Formal Mathematical property (FMP):
Abelian_group_set ( Abelian_group ( S , star , id , inv ) ) = S
Signatures:
sts


[Next: Abelian_group_operation] [Previous: Abelian_group] [Top]

Abelian_group_operation

Description:

This symbol takes one argument which should be an Abelian group. It returns a binary function, which represents the operation of the Abelian group.

Commented Mathematical property (CMP):
The operation of the Abelian group (S,*,1,inv) = *
Formal Mathematical property (FMP):
Abelian_group_operation ( Abelian_group ( S , star , id , inv ) ) = star
Signatures:
sts


[Next: Abelian_group_identity] [Previous: Abelian_group_set] [Top]

Abelian_group_identity

Description:

This symbol takes one argument which should be an Abelian group. It returns the identity of the Abelian group.

Commented Mathematical property (CMP):
The identity of the Abelian group (S,*,1,inv) = 1
Formal Mathematical property (FMP):
Abelian_group_identity ( Abelian_group ( S , star , id , inv ) ) = id
Signatures:
sts


[Next: Abelian_group_inverse] [Previous: Abelian_group_operation] [Top]

Abelian_group_inverse

Description:

This symbol takes one argument which should be an Abelian group. It reurns a unary function, which should be the inverse function for the Abelian group.

Commented Mathematical property (CMP):
The inverse of the Abelian group (S,*,1,inv) = inv
Formal Mathematical property (FMP):
Abelian_group_inverse ( Abelian_group ( S , star , id , inv ) ) = inv
Signatures:
sts


[Next: ordered_Abelian_group] [Previous: Abelian_group_identity] [Top]

ordered_Abelian_group

Description:

This symbol is the constructor for ordered Abelian groups, that is an Abelian group on which there is an ordering relation. The ordered_Abelian_group constructor takes five arguments, the set of the ordered Abelian group, a binary function taking two elements of the set into itself to represent the operation of the ordered Abelian group, an element of the set to represent the identity of the ordered Abelian group, a unary function taking the set into itself to specify inverse elements and a binary function taking two elements of the set into the booleans to specify the ordering of the ordered Abelian group.

Commented Mathematical property (CMP):
This constructor builds ordered Abelian groups
Formal Mathematical property (FMP):
ordered_Abelian_group ( S , star , id , inv , leq ) ordered_Abelian_group
Commented Mathematical property (CMP):
if (S,*,1,inv:S->S,\leq) represents an ordered Abelian group, then for all a,b in S | a \leq b or b \leq a and for all a,b,c in S | if a\leq b and b\leq c then a\leq c and for all a,b in S | if a\leq b and b\leq a then a=b
Formal Mathematical property (FMP):
S ordered_Abelian_group a , b . a ordered_Abelian_group_set ( S ) b ordered_Abelian_group_set ( S ) ( ordered_Abelian_group_order ( S ) ) ( a , b ) ( ordered_Abelian_group_order ( S ) ) ( b , a ) a , b , c . a ordered_Abelian_group_set ( S ) b ordered_Abelian_group_set ( S ) c ordered_Abelian_group_set ( S ) ( ordered_Abelian_group_order ( S ) ) ( a , b ) ( ordered_Abelian_group_order ( S ) ) ( b , c ) ( ordered_Abelian_group_order ( S ) ) ( a , c ) a , b . a ordered_Abelian_group_set ( S ) b ordered_Abelian_group_set ( S ) ( ordered_Abelian_group_order ( S ) ) ( a , b ) ( ordered_Abelian_group_order ( S ) ) ( b , a ) a = b
Signatures:
sts


[Next: ordered_Abelian_group_set] [Previous: Abelian_group_inverse] [Top]

ordered_Abelian_group_set

Description:

This symbol takes one argument which should be an ordered Abelian group. It returns the set of the ordered Abelian group.

Commented Mathematical property (CMP):
The set of the ordered Abelian group (S,*,1,inv,leq) = S
Formal Mathematical property (FMP):
ordered_Abelian_group_set ( ordered_Abelian_group ( S , star , id , inv , leq ) ) = S
Signatures:
sts


[Next: ordered_Abelian_group_operation] [Previous: ordered_Abelian_group] [Top]

ordered_Abelian_group_operation

Description:

This symbol takes one argument which should be an ordered Abelian group. It returns a binary function, which represents the operation of the ordered Abelian group.

Commented Mathematical property (CMP):
The operation of the ordered Abelian group (S,*,1,inv,leq) = *
Formal Mathematical property (FMP):
ordered_Abelian_group_operation ( ordered_Abelian_group ( S , star , id , inv , leq ) ) = star
Signatures:
sts


[Next: ordered_Abelian_group_identity] [Previous: ordered_Abelian_group_set] [Top]

ordered_Abelian_group_identity

Description:

This symbol takes one argument which should be an ordered Abelian group. It returns the identity of the ordered Abelian group.

Commented Mathematical property (CMP):
The identity of the ordered Abelian group (S,*,1,inv,leq) = 1
Formal Mathematical property (FMP):
ordered_Abelian_group_identity ( ordered_Abelian_group ( S , star , id , inv , leq ) ) = id
Signatures:
sts


[Next: ordered_Abelian_group_inverse] [Previous: ordered_Abelian_group_operation] [Top]

ordered_Abelian_group_inverse

Description:

This symbol takes one argument which should be an ordered Abelian group. It returns a unary function, which is the inverse function of the ordered Abelian group.

Commented Mathematical property (CMP):
The inverse of the ordered Abelian group (S,*,1,inv,leq) = inv
Formal Mathematical property (FMP):
ordered_Abelian_group_inverse ( ordered_Abelian_group ( S , star , id , inv , leq ) ) = inv
Signatures:
sts


[Next: ordered_Abelian_group_order] [Previous: ordered_Abelian_group_identity] [Top]

ordered_Abelian_group_order

Description:

This symbol takes one argument which should be an ordered Abelian group. It returns a binary function, which should represent the ordering of the ordered Abelian group.

Commented Mathematical property (CMP):
The order of the ordered Abelian group (S,*,1,inv,leq) = leq
Formal Mathematical property (FMP):
ordered_Abelian_group_order ( ordered_Abelian_group ( S , star , id , inv , leq ) ) = leq
Signatures:
sts


[Next: ringoid] [Previous: ordered_Abelian_group_inverse] [Top]

ringoid

Description:

This symbol is the constructor for ringoids. A ringoid is a set together with two operations + and *. * is left and right distributive over +. The ringoid constructor takes three arguments, the set of the ringoid, a binary function from the set into itself to represent the * operation and a binary function from the set into itself to represent the + operation.

Commented Mathematical property (CMP):
The ringoid constructor builds ringoids
Formal Mathematical property (FMP):
ringoid ( S , times , plus ) ringoid
Commented Mathematical property (CMP):
if (a,*,+) comprises a ringoid then for all a,b,c in S | a*(b+c) = a*b+a*c
Formal Mathematical property (FMP):
S ringoid a , b , c . a ringoid_set ( S ) b ringoid_set ( S ) c ringoid_set ( S ) ( ringoid_times ( S ) ) ( a , ( ringoid_plus ( S ) ) ( b , c ) ) = ( ringoid_plus ( S ) ) ( ( ringoid_times ( S ) ) ( a , b ) , ( ringoid_times ( S ) ) ( a , c ) )
Commented Mathematical property (CMP):
(b+c)*a = b*a+c*a
Formal Mathematical property (FMP):
S ringoid a , b , c . a ringoid_set ( S ) b ringoid_set ( S ) c ringoid_set ( S ) ( ringoid_times ( S ) ) ( ( ringoid_plus ( S ) ) ( b , c ) , a ) = ( ringoid_plus ( S ) ) ( ( ringoid_times ( S ) ) ( b , a ) , ( ringoid_times ( S ) ) ( c , a ) )
Signatures:
sts


[Next: ringoid_set] [Previous: ordered_Abelian_group_order] [Top]

ringoid_set

Description:

This symbol takes one argument which should be a ringoid. It returns a set which represents the set of the ringoid.

Commented Mathematical property (CMP):
The set of the ringoid (S,*,+) = S
Formal Mathematical property (FMP):
ringoid_set ( ringoid ( S , times , plus ) ) = S
Signatures:
sts


[Next: ringoid_times] [Previous: ringoid] [Top]

ringoid_times

Description:

This symbol takes one argument which should be a ringoid. It returns a binary function which represents the multiplicative operation (*) of the ringoid.

Commented Mathematical property (CMP):
The mulitplication operation of the ringoid (S,*,+) = S
Formal Mathematical property (FMP):
ringoid_times ( ringoid ( S , times , plus ) ) = times
Signatures:
sts


[Next: ringoid_plus] [Previous: ringoid_set] [Top]

ringoid_plus

Description:

This symbol takes one argument which should be a ringoid. It returns a binary function which represents the additive operation (+) of the ringoid.

Commented Mathematical property (CMP):
The addition operation of the ringoid (S,*,+) = +
Formal Mathematical property (FMP):
ringoid_plus ( ringoid ( S , times , plus ) ) = plus
Signatures:
sts


[Next: ring] [Previous: ringoid_times] [Top]

ring

Description:

This symbol is the constructor for rings. A ring is a set together with two operations + and *. A ring is an Abelian group under + and a semigroup under *. A ring has a further rule which associates the two operation, that is left and right distributivity. The ring constructor takes five arguments, the set of the ring, a binary function from the set into itself to represent the * operation, a binary function from the set into itself to represent the + operation, an element of the set of the ring to represent the additive identity 0 and a unary function from the set into itself to represent additive inverses (i.e. inverses under +, or negatives).

Commented Mathematical property (CMP):
This constructor builds rings
Formal Mathematical property (FMP):
ring ( S , times , plus , zero , neg ) ring
Commented Mathematical property (CMP):
A ring is a ringoid
Commented Mathematical property (CMP):
if (S,*,+,0,neg:S->S) comprises a ring then * is both left and right distributive over +. That is: For all a,b,c in S, a*(b+c)=(a*b)+(a*c) and (b+c)*a=(b*a)+(c*a)
Formal Mathematical property (FMP):
S ring a , b , c . a ring_set ( S ) b ring_set ( S ) c ring_set ( S ) ( ring_times ( S ) ) ( a , ( ring_plus ( S ) ) ( b , c ) ) = ( ring_plus ( S ) ) ( ( ring_times ( S ) ) ( a , b ) , ( ring_times ( S ) ) ( a , c ) ) = ( ring_times ( S ) ) ( ( ring_plus ( S ) ) ( b , c ) , a ) = ( ring_plus ( S ) ) ( ( ring_times ( S ) ) ( b , a ) , ( ring_times ( S ) ) ( c , a ) )
Signatures:
sts


[Next: ring_set] [Previous: ringoid_plus] [Top]

ring_set

Description:

This symbol takes one argument which should be a ring. It returns the set of the ring.

Commented Mathematical property (CMP):
The set of the ring (S,*,+,0,neg) = S
Formal Mathematical property (FMP):
ring_set ( ring ( S , times , plus , zero , neg ) ) = S
Signatures:
sts


[Next: ring_times] [Previous: ring] [Top]

ring_times

Description:

This symbol takes one argument which should be a ring. It returns a binary function which represents the multiplicative operation of the ring.

Commented Mathematical property (CMP):
The times of the ring (S,*,+,0,neg) = *
Formal Mathematical property (FMP):
ring_times ( ring ( S , times , plus , zero , neg ) ) = times
Signatures:
sts


[Next: ring_plus] [Previous: ring_set] [Top]

ring_plus

Description:

This symbol takes one argument which should be a ring. It returns a binary function which represents the additive operation of the ring.

Commented Mathematical property (CMP):
The plus of the ring (S,*,+,0,neg) = +
Formal Mathematical property (FMP):
ring_plus ( ring ( S , times , plus , zero , neg ) ) = plus
Signatures:
sts


[Next: ring_zero] [Previous: ring_times] [Top]

ring_zero

Description:

This symbol takes one argument which should be a ring. It returns the additive identity of the ring.

Commented Mathematical property (CMP):
The zero of the ring (S,*,+,0,neg) = 0
Formal Mathematical property (FMP):
ring_zero ( ring ( S , times , plus , zero , neg ) ) = zero
Signatures:
sts


[Next: ring_negative] [Previous: ring_plus] [Top]

ring_negative

Description:

This symbol takes one argument which should be a ring. It returns a unary function which should be the negative function of the ring.

Commented Mathematical property (CMP):
The negative function of the ring (S,*,+,0,neg) = neg
Formal Mathematical property (FMP):
ring_negative ( ring ( S , times , plus , zero , neg ) ) = neg
Signatures:
sts


[Next: ordered_ring] [Previous: ring_zero] [Top]

ordered_ring

Description:

This symbol is the constructor for ordered rings, that is a ring on which there is an ordering relation. The ordered_ring constructor takes six arguments, the set of the ordered ring, a binary function from the set into itself to represent the multiplicative operation (*), a binary function from the set into itself to represent the additive operation (+), an element of the set of the ordered ring to represent the additive identity 0, a unary function from the set into itself to represent additive inverses (i.e. inverses under +, or negatives) and a binary function from the set into the booleans to represent the ordering relation.

Commented Mathematical property (CMP):
This constructor builds ordered rings
Formal Mathematical property (FMP):
ordered_ring ( S , times , plus , zero , neg , leq ) ordered_ring
Commented Mathematical property (CMP):
if (S,*,+,0,neg:S->S,\leq) constitutes an ordered ring, then for all a,b in S | a \leq b or b \leq a and for all a,b,c in S | if a\leq b and b\leq c then a\leq c and for all a,b in S | if a\leq b and b\leq a then a=b
Formal Mathematical property (FMP):
S ordered_ring a , b . a ordered_ring_set ( S ) b ordered_ring_set ( S ) ( ordered_ring_order ( S ) ) ( a , b ) ( ordered_ring_order ( S ) ) ( b , a ) a , b , c . a ordered_ring_set ( S ) b ordered_ring_set ( S ) c ordered_ring_set ( S ) ( ordered_ring_order ( S ) ) ( a , b ) ( ordered_ring_order ( S ) ) ( b , c ) ( ordered_ring_order ( S ) ) ( a , c ) a , b . a ordered_ring_set ( S ) b ordered_ring_set ( S ) ( ordered_ring_order ( S ) ) ( a , b ) ( ordered_ring_order ( S ) ) ( b , a ) a = b
Signatures:
sts


[Next: ordered_ring_set] [Previous: ring_negative] [Top]

ordered_ring_set

Description:

This symbol takes one argument which should be an ordered ring. It returns the set of the ordered ring.

Commented Mathematical property (CMP):
The set of the ordered ring (S,*,+,0,-,leq) = *
Formal Mathematical property (FMP):
ordered_ring_set ( ordered_ring ( S , times , plus , zero , neg , leq ) ) = S
Signatures:
sts


[Next: ordered_ring_times] [Previous: ordered_ring] [Top]

ordered_ring_times

Description:

This symbol takes one argument which should be an ordered ring. It returns a binary function, which represents the multiplicative operation of the ordered ring.

Commented Mathematical property (CMP):
The times of the ordered ring (S,*,+,0,-,leq) = *
Formal Mathematical property (FMP):
ordered_ring_times ( ordered_ring ( S , times , plus , zero , neg , leq ) ) = times
Signatures:
sts


[Next: ordered_ring_plus] [Previous: ordered_ring_set] [Top]

ordered_ring_plus

Description:

This symbol takes one argument which should be an ordered ring. It returns a binary function, which represents the additive operation of the ordered ring.

Commented Mathematical property (CMP):
The + of the ordered ring (S,*,+,0,-,leq) = +
Formal Mathematical property (FMP):
ordered_ring_plus ( ordered_ring ( S , times , plus , zero , neg , leq ) ) = plus
Signatures:
sts


[Next: ordered_ring_zero] [Previous: ordered_ring_times] [Top]

ordered_ring_zero

Description:

This symbol takes one argument which should be an ordered ring. It returns the zero of the ordered ring.

Commented Mathematical property (CMP):
The zero of the ordered ring (S,*,+,0,-,leq) = 0
Formal Mathematical property (FMP):
ordered_ring_zero ( ordered_ring ( S , times , plus , zero , neg , leq ) ) = zero
Signatures:
sts


[Next: ordered_ring_negative] [Previous: ordered_ring_plus] [Top]

ordered_ring_negative

Description:

This symbol takes one argument which should be an ordered ring. It returns a unary function to represent the additive inverse function of the ordered ring.

Commented Mathematical property (CMP):
The negative of the ordered ring (S,*,+,0,-,leq) = -
Formal Mathematical property (FMP):
ordered_ring_negative ( ordered_ring ( S , times , plus , zero , neg , leq ) ) = neg
Signatures:
sts


[Next: ordered_ring_order] [Previous: ordered_ring_zero] [Top]

ordered_ring_order

Description:

This symbol takes one argument which should be an ordered ring. It returns a binary function, which represents the order function on the ordered ring.

Commented Mathematical property (CMP):
The order of the ordered ring (S,*,+,0,-,leq) = leq
Formal Mathematical property (FMP):
ordered_ring_order ( ordered_ring ( S , times , plus , zero , neg , leq ) ) = leq
Signatures:
sts


[Next: non_commutative_ring] [Previous: ordered_ring_negative] [Top]

non_commutative_ring

Description:

This symbol is the constructor for non commutative rings, these are rings over which the * operator is not commutative. the non_commutative_ring constructor takes five arguments: The set of the non-commutative ring. A binary function into itself to represent the multiplication operation, *. A binary function into itself to represent the addition operation, +. A member of the set of the non-commutative ring to specify the additive identity, 0. And a unary function taking the set of the non-commutative ring into itself to represent the additive inverses of the non-commutative ring (i.e. inverses under +, or negatives).

Commented Mathematical property (CMP):
This constructor builds non-commutative rings
Formal Mathematical property (FMP):
non_commutative_ring ( S , times , plus , zero , neg ) non_commutative_ring
Commented Mathematical property (CMP):
if (S,*,+,0,neg:S->S) constitutes a non-commutative ring, then there exist a,b in S such that a*b~=b*a
Formal Mathematical property (FMP):
S non_commutative_ring a , b . a non_commutative_ring_set ( S ) b non_commutative_ring_set ( S ) ( non_commutative_ring_times ( S ) ) ( a , b )
Signatures:
sts


[Next: non_commutative_ring_set] [Previous: ordered_ring_order] [Top]

non_commutative_ring_set

Description:

This symbol takes one argument which should be a non-commutative ring. It returns the set of the non-commutative ring.

Commented Mathematical property (CMP):
The set of the non-commutative ring (S,*,+,0,-) = S
Formal Mathematical property (FMP):
non_commutative_ring_set ( non_commutative_ring ( S , times , plus , zero , neg ) ) = S
Signatures:
sts


[Next: non_commutative_ring_times] [Previous: non_commutative_ring] [Top]

non_commutative_ring_times

Description:

This symbol takes one argument which should be a non-commutative ring. It returns a binary function, which represents the multiplicative function of the non-commutative ring.

Commented Mathematical property (CMP):
The times of the non-commutative ring (S,*,+,0,-) = *
Formal Mathematical property (FMP):
non_commutative_ring_times ( non_commutative ( S , times , plus , zero , neg ) ) = times
Signatures:
sts


[Next: non_commutative_ring_plus] [Previous: non_commutative_ring_set] [Top]

non_commutative_ring_plus

Description:

This symbol takes one argument which should be a non-commutative ring. It returns a binary function, which represents the additive function of the non-commutative ring.

Commented Mathematical property (CMP):
The plus of the non-commutative ring (S,*,+,0,-) = +
Formal Mathematical property (FMP):
non_commutative_ring_plus ( non_commutative_ring ( S , times , plus , zero , neg ) ) = plus
Signatures:
sts


[Next: non_commutative_ring_zero] [Previous: non_commutative_ring_times] [Top]

non_commutative_ring_zero

Description:

This symbol takes one argument which should be a non-commutative ring. It returns the zero of the non-commutative ring.

Commented Mathematical property (CMP):
The zero of the non-commutative ring (S,*,+,0,-) = 0
Formal Mathematical property (FMP):
non_commutative_ring_zero ( non_commutative_ring ( S , times , plus , zero , neg ) ) = zero
Signatures:
sts


[Next: non_commutative_ring_negative] [Previous: non_commutative_ring_plus] [Top]

non_commutative_ring_negative

Description:

This symbol takes one argument which should be a non-commutative ring. It returns a unary function, which represents the multiplicative inverse of the non-commutative ring.

Commented Mathematical property (CMP):
The negative of the non-commutative ring (S,*,+,0,-) = -
Formal Mathematical property (FMP):
non_commutative_ring_negative ( non_commutative_ring ( S , times , plus , zero , neg ) ) = neg
Signatures:
sts


[Next: Euclidean_domain] [Previous: non_commutative_ring_zero] [Top]

Euclidean_domain

Description:

This symbol is the constructor for Euclidean domains. A Euclidean domain is a ring on which there is no zero divisors together with an integer norm function. The Euclidean_domain constructor takes six arguments: The set of the Euclidean domain. A binary function into itself to represent the multiplication operation, *. A binary function into itself to represent the addition operation, +. A member of the set of the Euclidean domain to specify the additive identity, 0. A unary function taking the set of the Euclidean domain into itself to represent the additive inverses (i.e. inverses under +, or negatives). And a unary function taking elements of the set into the positive integers, to represent the integer norm function.

Commented Mathematical property (CMP):
This constructor builds Euclidean domains
Formal Mathematical property (FMP):
Euclidean_domain ( S , times , plus , zero , neg , abs ) Euclidean_domain
Commented Mathematical property (CMP):
if (S,*,+,0,neg:S->S,abs:S->Z^+) constitutes a Euclidean domain then for every a,b ~= 0 in S then abs(a*b) >= abs(a) and abs(a*b) >= abs(b) and for every a,b ~= 0 in S then there exists q and r in S such that a=q*b + r and abs(r) < abs(B) or r=0
Formal Mathematical property (FMP):
S Euclidean_domain a , b . a Euclidean_domain_set ( S ) b Euclidean_domain_set ( S ) a Euclidean_domain_zero ( S ) b Euclidean_domain_zero ( S ) ( Euclidean_domain_abs ( S ) ) ( ( Euclidean_domain_times ( S ) ) ( a , b ) ) Euclidean_domain_abs ( S ) a ( Euclidean_domain_abs ( S ) ) ( ( Euclidean_domain_times ( S ) ) ( a , b ) ) ( Euclidean_domain_abs ( S ) ) ( b ) a , b . a Euclidean_domain_set ( S ) b Euclidean_domain_set ( S ) a Euclidean_domain_zero ( S ) b Euclidean_domain_zero ( S ) q , r . ( r = Euclidean_domain_zero ( S ) ) ( q Euclidean_domain_set ( S ) r Euclidean_domain_set ( S ) a = ( Euclidean_domain_plus ( S ) ) ( ( Euclidean_domain_times ( S ) ) ( q , b ) , r ) ( Euclidean_domain_abs ( S ) ) ( r ) < ( Euclidean_domain_abs ( S ) ) ( b ) )
Signatures:
sts


[Next: Euclidean_domain_set] [Previous: non_commutative_ring_negative] [Top]

Euclidean_domain_set

Description:

This symbol takes one argument which should be a Euclidean domain. It returns the set of the Euclidean domain.

Commented Mathematical property (CMP):
The set of the Euclidean domain (S,*,+,0,-,abs) = S
Formal Mathematical property (FMP):
Euclidean_domain_set ( Euclidean_domain ( S , times , plus , zero , neg , abs ) ) = S
Signatures:
sts


[Next: Euclidean_domain_times] [Previous: Euclidean_domain] [Top]

Euclidean_domain_times

Description:

This symbol takes one argument which should be a Euclidean domain. It returns a binary function, which represents the multiplicative operation of the Euclidean domain.

Commented Mathematical property (CMP):
The times of the Euclidean domain (S,*,+,0,-,abs) = *
Formal Mathematical property (FMP):
Euclidean_domain_times ( Euclidean_domain ( S , times , plus , zero , neg , abs ) ) = times
Signatures:
sts


[Next: Euclidean_domain_plus] [Previous: Euclidean_domain_set] [Top]

Euclidean_domain_plus

Description:

This symbol takes one argument which should be a Euclidean domain. It returns a binary function, which represents the additive operation of the Euclidean domain.

Commented Mathematical property (CMP):
The plus of the Euclidean domain (S,*,+,0,-,abs) = +
Formal Mathematical property (FMP):
Euclidean_domain_plus ( Euclidean_domain_plus ( S , times , plus , zero , neg , abs ) ) = plus
Signatures:
sts


[Next: Euclidean_domain_zero] [Previous: Euclidean_domain_times] [Top]

Euclidean_domain_zero

Description:

This symbol takes one argument which should be a Euclidean domain. It returns the additive identity of the Euclidean domain.

Commented Mathematical property (CMP):
The zero of the Euclidean domain (S,*,+,0,-,abs) = 0
Formal Mathematical property (FMP):
Euclidean_domain_zero ( Euclidean_domain ( S , times , plus , zero , neg , abs ) ) = zero
Signatures:
sts


[Next: Euclidean_domain_negative] [Previous: Euclidean_domain_plus] [Top]

Euclidean_domain_negative

Description:

This symbol takes one argument which should be a Euclidean domain. It returns a unary function, which represents additive inverses of the Euclidean domain.

Commented Mathematical property (CMP):
The negative of the Euclidean domain (S,*,+,0,-,abs) = -
Formal Mathematical property (FMP):
Euclidean_domain_negative ( Euclidean_domain ( S , times , plus , zero , neg , abs ) ) = neg
Signatures:
sts


[Next: Euclidean_domain_abs] [Previous: Euclidean_domain_zero] [Top]

Euclidean_domain_abs

Description:

This symbol takes one argument which should be a Euclidean domain. It returns a unary function, which is the absolute value function of the Euclidean domain.

Commented Mathematical property (CMP):
The absolute value function of the Euclidean domain (S,*,+,0,-,abs) = abs
Formal Mathematical property (FMP):
Euclidean_domain_abs ( Euclidean_domain ( S , times , plus , zero , neg , abs ) ) = abs
Signatures:
sts


[Next: field] [Previous: Euclidean_domain_negative] [Top]

field

Description:

This symbol is the constructor for fields. A field is an Abelian group under +, the set of the field complement {0} with * is an Abelian group, a field has a further rule which associates the two operations, that is left and right distributivity. The field constructor takes seven arguments: The set of the field. A binary function into itself to represent the multiplication operation, *. A binary function into itself to represent the addition operation, +. A member of the set of the field to specify the multiplicative identity, 1. A member of the set of the field to specify the additive identity, 0. A unary function taking the set of the field into itself to represent the multiplicative inverses (i.e. inverses under *). A unary function taking the set of the field into itself to represent the additive inverses (i.e. inverses under +, or negatives).

Commented Mathematical property (CMP):
This constructor builds fields
Formal Mathematical property (FMP):
fields ( S , times , plus , one , zero , inv , neg ) fields
Commented Mathematical property (CMP):
The set of the field complement {0} with * is an Abelian group
Formal Mathematical property (FMP):
S field field_set ( S ) { field_zero ( ) } Abelian_group
Signatures:
sts


[Next: field_set] [Previous: Euclidean_domain_abs] [Top]

field_set

Description:

This symbol takes one argument which should be a field. It returns the set of the field.

Commented Mathematical property (CMP):
The set of the field (S,*,+,1,0,inv,-) = S
Formal Mathematical property (FMP):
field_set ( field ( S , times , plus , one , zero , inv , neg ) ) = S
Signatures:
sts


[Next: field_times] [Previous: field] [Top]

field_times

Description:

This symbol takes one argument which should be a field. It returns a binary function, to represent the multiplicative operation of the field.

Commented Mathematical property (CMP):
The times of the field (S,*,+,1,0,inv,-) = *
Formal Mathematical property (FMP):
field_times ( field ( S , times , plus , one , zero , inv , neg ) ) = times
Signatures:
sts


[Next: field_plus] [Previous: field_set] [Top]

field_plus

Description:

This symbol takes one argument which should be a field. It returns a binary function, to represent the additive operation of the field.

Commented Mathematical property (CMP):
The plus of the field (S,*,+,1,0,inv,-) = +
Formal Mathematical property (FMP):
field_plus ( field ( S , times , plus , one , zero , inv , neg ) ) = plus
Signatures:
sts


[Next: field_one] [Previous: field_times] [Top]

field_one

Description:

This symbol takes one argument which should be a field. It returns the multiplicative identity of the field.

Commented Mathematical property (CMP):
The one of the field (S,*,+,1,0,inv,-) = 1
Formal Mathematical property (FMP):
field_one ( field ( S , times , plus , one , zero , inv , neg ) ) = one
Signatures:
sts


[Next: field_zero] [Previous: field_plus] [Top]

field_zero

Description:

This symbol takes one argument which should be a field. It returns the additive identity of the field.

Commented Mathematical property (CMP):
The zero of the field (S,*,+,1,0,inv,-) = 0
Formal Mathematical property (FMP):
field_zero ( field ( S , times , plus , one , zero , inv , neg ) ) = zero
Signatures:
sts


[Next: field_reciprocal] [Previous: field_one] [Top]

field_reciprocal

Description:

This symbol takes one argument which should be a field. It returns a unary function, which is the multiplicative inverse function of the field.

Commented Mathematical property (CMP):
The reciprocal of the field (S,*,+,1,0,inv,-) = inv
Formal Mathematical property (FMP):
field_reciprocal ( field ( S , times , plus , one , zero , inv , neg ) ) = inv
Signatures:
sts


[Next: field_negative] [Previous: field_zero] [Top]

field_negative

Description:

This symbol takes one argument which should be a field. It returns a unary function, which is the additive inverse function of the field.

Commented Mathematical property (CMP):
The negative of the field (S,*,+,1,0,inv,-) = -
Formal Mathematical property (FMP):
field_negative ( field ( S , times , plus , one , zero , inv , neg ) ) = neg
Signatures:
sts


[Next: integral_domain] [Previous: field_reciprocal] [Top]

integral_domain

Description:

This symbol is the constructor for integral domains. An integral domain is a ring which is commutative under *, it has a multiplicative identity (under *), and has no zero divisors. The integral_domain constructor takes six arguments. The set of the integral domain, a binary function from the set into itself to represent the * operation, a binary function from the set into itself to represent the + operation, an element of the set of the ring to represent the multiplicative identity 1, an element of the set of the ring to represent the additive identity 0, and a unary function from the set into itself to represent additive inverses (i.e. inverses under +, or negatives).

Commented Mathematical property (CMP):
This constructor builds integral domains
Formal Mathematical property (FMP):
integral_domain ( S , times , one , plus , zero , neg ) integral_domain
Commented Mathematical property (CMP):
An integral domain is commutative under *
Formal Mathematical property (FMP):
S integral_domain a , b . a integral_domain_set ( S ) b integral_domain_set ( S ) ( integral_domain_times ( S ) ) ( a , b ) = ( integral_domain_times ( S ) ) ( b , a )
Commented Mathematical property (CMP):
An integral domain has a multiplicative identity
Formal Mathematical property (FMP):
S integral_domain id . x . ( integral_domain_times ( S ) ) ( id , x ) = x ( integral_domain_times ( S ) ) ( x , id ) = x
Commented Mathematical property (CMP):
An integral domain has no zero divisors
Formal Mathematical property (FMP):
S integral_domain ¬ zerodiv . x integral_domain_set ( S ) x integral_domain_zero ( S ) ( integral_domain_times ( S ) ) ( zerodiv , x )
Signatures:
sts


[Next: integral_domain_set] [Previous: field_negative] [Top]

integral_domain_set

Description:

This symbol takes one argument which should be an integral domain. It returns the set of the integral domain.

Commented Mathematical property (CMP):
The set of the integral domain (S,*,+,1,0,-) = S
Formal Mathematical property (FMP):
integral_domain_set ( integral_domain ( S , times , plus , one , zero , neg ) ) = S
Signatures:
sts


[Next: integral_domain_times] [Previous: integral_domain] [Top]

integral_domain_times

Description:

This symbol takes one argument which should be an integral domain. It returns a binary function which represents the multiplicative operation of the integral domain.

Commented Mathematical property (CMP):
The times of the integral domain (S,*,+,1,0,-) = *
Formal Mathematical property (FMP):
integral_domain_times ( integral_domain ( S , times , plus , one , zero , neg ) ) = times
Signatures:
sts


[Next: integral_domain_plus] [Previous: integral_domain_set] [Top]

integral_domain_plus

Description:

This symbol takes one argument which should be an integral domain. It returns a binary function which represents the additive operation of the integral domain.

Commented Mathematical property (CMP):
The plus of the integral domain (S,*,+,1,0,-) = +
Formal Mathematical property (FMP):
integral_domain_plus ( integral_domain ( S , times , plus , one , zero , neg ) ) = plus
Signatures:
sts


[Next: integral_domain_one] [Previous: integral_domain_times] [Top]

integral_domain_one

Description:

This symbol takes one argument which should be an integral domain. It returns the multiplicative identity of the integral domain.

Commented Mathematical property (CMP):
The one of the integral domain (S,*,+,1,0,-) = 1
Formal Mathematical property (FMP):
integral_domain_one ( integral_domain ( S , times , plus , one , zero , neg ) ) = one
Signatures:
sts


[Next: integral_domain_zero] [Previous: integral_domain_plus] [Top]

integral_domain_zero

Description:

This symbol takes one argument which should be an integral domain. It returns the additive identity of the integral domain.

Commented Mathematical property (CMP):
The zero of the integral domain (S,*,+,1,0,-) = 0
Formal Mathematical property (FMP):
integral_domain_zero ( integral_domain ( S , times , plus , one , zero , neg ) ) = zero
Signatures:
sts


[Next: integral_domain_negative] [Previous: integral_domain_one] [Top]

integral_domain_negative

Description:

This symbol takes one argument which should be an integral domain. It returns a unary function which represents the additive inverse function of the integral domain.

Commented Mathematical property (CMP):
The negative of the integral domain (S,*,+,1,0,-) = -
Formal Mathematical property (FMP):
integral_domain_negative ( integral_domain ( S , times , plus , one , zero , neg ) ) = neg
Signatures:
sts


[First: monoid] [Previous: integral_domain_zero] [Top]