Reference · Vectors

rainbow.math.linear.vector.dot-commutative

Vectorssrc/rainbow/math/linear/vector/dot_commutative.clj0 definitions, 1 theorems

Commutativity of the native truncating signed-vector dot product. dot left right ~ dot right left If either list is empty both orientations reduce to signed zero. The cons/cons case combines signed multiplication commutativity at the head with the tail induction hypothesis through signed addition congruence. Native and axiom-free on D63.

Depends onmath.rational.signed.multiply

vector/dot-commutative :
  (left right : List ℚ)
  → vector/dot left right = vector/dot right left