Relation DIVISION-RING

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

Slots on this relation:

Instance-Of: Relation

Arity: 5

Subrelation-Of: Ring

Equivalence Axioms:

(<=> (Division-Ring ?Domain ?Plus-Op ?Zero-Id ?Mult-Op ?One-Id)
     (And (Ring ?Domain ?Plus-Op ?Zero-Id ?Mult-Op ?One-Id)
          (Group (Kappa (?X)
                        (And (Instance-Of ?X ?Domain)
                             (/= ?X ?Zero-Id)))
                 ?Mult-Op
                 ?One-Id)))

Other Related Axioms:

(<=> (Division-Ring ?Domain ?Plus-Op ?Zero-Id ?Mult-Op ?One-Id)
     (And (Ring ?Domain ?Plus-Op ?Zero-Id ?Mult-Op ?One-Id)
          (Group (Kappa (?X)
                        (And (Instance-Of ?X ?Domain)
                             (/= ?X ?Zero-Id)))
                 ?Mult-Op
                 ?One-Id)))

(Subrelation-Of Field Division-Ring)

(<=> (Field ?Domain ?Plus-Op ?Zero-Id ?Mult-Op ?One-Id)
     (And (Division-Ring ?Domain ?Plus-Op ?Zero-Id ?Mult-Op ?One-Id)
          (Commutative ?Plus-Op ?Domain)))