Relation INTEGRAL-DOMAIN

• Defined in theory: Abstract-algebra
• Source code: abstract-algebra.lisp

Slots on this relation:

Instance-Of: Relation

Arity: 5

Subrelation-Of: Commutative-ring

Equivalence Axioms:

(<=> (Integral-Domain ?Domain ?Plus-Op ?Zero-Id ?Mult-Op ?One-Id)
     (And (Commutative-Ring ?Domain
                            ?Plus-Op
                            ?Zero-Id
                            ?Mult-Op
                            ?One-Id)
          (Binary-Operator-On ?Mult-Op
                              (Kappa (?X)
                                     (And (Instance-Of ?X ?Domain)
                                          (/= ?X ?Zero-Id))))))

Other Related Axioms:

(<=> (Integral-Domain ?Domain ?Plus-Op ?Zero-Id ?Mult-Op ?One-Id)
     (And (Commutative-Ring ?Domain
                            ?Plus-Op
                            ?Zero-Id
                            ?Mult-Op
                            ?One-Id)
          (Binary-Operator-On ?Mult-Op
                              (Kappa (?X)
                                     (And (Instance-Of ?X ?Domain)
                                          (/= ?X ?Zero-Id))))))