(<=> (Scalar-Quantity ?Q)
(And (Constant-Quantity ?Q)
(Forall (?U)
(=> (And (Unit-Of-Measure ?U)
(Compatible-Quantities ?U ?Q))
(Real-Number (Magnitude ?Q ?U))))))
(Identity-Element-For Identity-Scalar * Scalar-Quantity)
(=> (And (Scalar-Quantity ?X) (Scalar-Quantity ?Y))
(<=> (+ ?X ?Y ?Z)
(And (Scalar-Quantity ?Z)
(Forall (?U)
(=> (And (Unit-Of-Measure ?U)
(Compatible-Quantities ?X ?U))
(= (+ (Magnitude ?X ?U) (Magnitude ?Y ?U))
(Magnitude ?Z ?U)))))))
(Abelian-Group
(Kappa (?X)
(And (Scalar-Quantity ?X)
(Forall (?Dim)
(=> (Physical-Dimension ?Dim)
(/= (The-Zero-Scalar-For-Dimension ?Dim)
?X)))))
*
1)
(=> (And (Scalar-Quantity ?X) (Scalar-Quantity ?Y))
(<=> (* ?X ?Y ?Z)
(And (Scalar-Quantity ?Z)
(Forall (?U ?U1 ?U2)
(=> (And (Unit-Of-Measure ?U)
(Compatible-Quantities ?X ?U)
(Unit-Of-Measure ?U1)
(Compatible-Quantities ?Y ?U1)
(Unit-Of-Measure ?U1)
(= (Quantity.Dimension ?U2)
(* (Quantity.Dimension ?U)
(Quantity.Dimension ?U1))))
(= (* (Magnitude ?X ?U1)
(Magnitude ?Y ?U2))
(Magnitude ?Z ?U)))))))
(=> (And (Scalar-Quantity ?X) (Recip ?X ?Y))
(And (Scalar-Quantity ?Y)
(Forall (?Dim)
(=> (/= ?X (The-Zero-Scalar-For-Dimension ?Dim))
(= (* ?X ?Y) Identity-Scalar)))))
(=> (And (Scalar-Quantity ?X) (Real-Number ?R) (Expt ?X ?R ?Z))
(And (Scalar-Quantity ?Z)
(=> (= ?R 0) (= ?Z 1))
(Forall (?U)
(=> (Unit-Of-Measure ?U)
(= (Expt (Magnitude ?X ?U) ?R)
(Magnitude ?Z (Expt ?U ?R)))))))
(<- (Scalar-Quantities-Of-Dimension ?Dimension)
(If (Physical-Dimension ?Dimension)
(Kappa (?Q)
(And (Scalar-Quantity ?Q)
(= (Quantity.Dimension ?Q) ?Dimension)))))
(=> (The-Zero-Scalar-For-Dimension $X $Y) (Scalar-Quantity $Y))
(=> (= (The-Zero-Scalar-For-Dimension ?Dimension) ?Zero-Scalar)
(Scalar-Quantity ?Zero-Scalar))