Function *


Slots on this function:

Documentation:
Multiplication of a vector-quantity by a scalar-quantity results in a vector-quantity. The product is equal to the vector-quantity constructed by multiplying each component of the argument vector by the argument scalar.

The * function is commutative for scalar/vector pairs.


Axioms:

(=> (And (Vector-Quantity ?V1) (Scalar-Quantity ?S))
    (= (* ?V1 ?S) (* ?S ?V1)))

(=> (And (Scalar-Quantity ?S) (Vector-Quantity ?V1) (* ?S ?V1 ?V))
    (And (Vector-Quantity ?V)
         (= (Spatial.Dimension ?V1) (Spatial.Dimension ?V))
         (Forall (?B ?I)
                 (=> (= (Basis.Dimension ?B) (Spatial.Dimension ?V1))
                     (= (Vector-Component ?V ?I ?B)
                        (* ?S (Vector-Component ?V1 ?I ?B)))))))