Relation IDENTITY-ELEMENT-FOR

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

Slots on this relation:

Documentation:

An object ?id is the identity element for binary operator ?o over domain ?d iff for every instance ?x of ?d, applying ?o to ?x and ?id results in ?x.

Instance-Of: Relation

Arity: 3

Equivalence Axioms:

(<=> (Identity-Element-For ?Id ?Op ?Domain)
     (And (Instance-Of ?Id ?Domain)
          (Binary-Operator-On ?Op ?Domain)
          (Forall (?X)
                  (=> (Instance-Of ?X ?Domain)
                      (= (Value ?Op ?Id ?X) ?X)))))

Other Related Axioms:

(<=> (Identity-Element-For ?Id ?Op ?Domain)
     (And (Instance-Of ?Id ?Domain)
          (Binary-Operator-On ?Op ?Domain)
          (Forall (?X)
                  (=> (Instance-Of ?X ?Domain)
                      (= (Value ?Op ?Id ?X) ?X)))))

(<=> (Semigroup ?Domain ?Op ?Id)
     (And (Binary-Operator-On ?Op ?Domain)
          (Associative ?Op ?Domain)
          (Identity-Element-For ?Id ?Op ?Domain)))

(<=> (Group ?Domain ?Op ?Id)
     (And (Binary-Operator-On ?Op ?Domain)
          (Associative ?Op ?Domain)
          (Identity-Element-For ?Id ?Op ?Domain)
          (Invertible ?Op ?Id ?Domain)))