Reference · Vectors

rainbow.math.linear.vector.add-reorder

Vectorssrc/rainbow/math/linear/vector/add_reorder.clj0 definitions, 2 theorems

Four-term reordering and additive distribution for vector subtraction. (a + b) + (c + d) ~ (a + c) + (b + d) (a + b) - (c + d) ~ (a - c) + (b - d) Both statements remain valid for truncating vector addition because all sides stop at the same minimum input dimension. Proofs compose existing checked vector algebra laws and add no recursion.

Depends onmath.linear.vector.subtract-negation

vector/add-four-reorder :
  (a b c d : List ℚ)
  → vector/equivalent (add) (add₁)
  where add := vector/add (vector/add a b) (vector/add c d)
  where add₁ := vector/add (vector/add a c) (vector/add b d)

vector/subtract-additive :
  (a b c d : List ℚ)
  → vector/equivalent (subtract) (add)
  where add := vector/add (vector/subtract a c) (vector/subtract b d)
  where subtract := vector/subtract (vector/add a b) (vector/add c d)