Physical-dimension IDENTITY-DIMENSION

• Defined in theory: Physical-quantities
• Source code: physical-quantities.lisp

Slots on this physical-dimension:

Documentation:

identity-dimension is the identity element for the * operator over physical-dimensions. That means that the product of identity-dimension and any other dimension is that other dimension. Identity-dimension is the dimension of the so-called dimensionless quantities, including the real numbers.

Instance-Of: Physical-dimension

Axioms:

(Identity-Element-For Identity-Dimension * Physical-Dimension)

Other Related Axioms:

(<= (Quantity.Dimension $X Identity-Dimension)
    (Dimensionless-Quantity $X))

(Inherited-Slot-Value Dimensionless-Quantity
                      Quantity.Dimension
                      Identity-Dimension)

(<=> (Dimensionless-Quantity ?X)
     (And (Constant-Quantity ?X)
          (= (Quantity.Dimension ?X) Identity-Dimension)))

(Forall (?D1 ?D2 ?R1 ?R2)
        (=> (And (Physical-Dimension ?D1)
                 (Physical-Dimension ?D2)
                 (Real-Number ?R1)
                 (Real-Number ?R2))
            (And (= (Expt ?D1 0) Identity-Dimension)
                 (= ?D1 (Expt ?D1 1))
                 (= (* (Expt ?D1 ?R1) (Expt ?D1 ?R2))
                    (Expt ?D1 (+ ?R1 ?R2)))
                 (= (Expt (* ?D1 ?D2) ?R1)
                    (* (Expt ?D1 ?R1) (Expt ?D2 ?R1)))
                 (= (Expt (Expt ?D1 ?R1) ?R2) (Expt ?D1 (* ?R1 ?R2))))))

(Abelian-Group Physical-Dimension * Identity-Dimension)

(= (Quantity.Dimension Identity-Unit) Identity-Dimension)