Reference · Vectors

rainbow.math.linear.vector.dot-subtract

Vectorssrc/rainbow/math/linear/vector/dot_subtract.clj0 definitions, 3 theorems

Subtraction laws for signed values and the native vector dot product. signed/subtract-respects-equivalence vector/dot-subtract-left vector/dot-subtract-right Native vector subtraction zips its arguments, so dot subtraction requires an explicit same-shape hypothesis: without it, the subtraction can discard a suffix that a separately computed dot product would retain. Under that hypothesis, left subtraction follows from dot additivity and dot negation; the right law follows by dot commutativity.

Depends onmath.linear.vector.dot-negatemath.linear.vector.shape-map

signed/subtract-respects-equivalence :
  (left left-prime right right-prime : ℚ)
  (left-same : left = left-prime)
  (right-same : right = right-prime)
  → left - right = left-prime - right-prime

vector/dot-subtract-left :
  (left right weights : List ℚ) (same : vector/same-shape left right)
  → vector/dot (vector/subtract left right) weights = vector/dot left weights - vector/dot right weights

vector/dot-subtract-right :
  (weights left right : List ℚ) (same : vector/same-shape left right)
  → vector/dot weights (vector/subtract left right) = vector/dot weights left - vector/dot weights right