Reference · Vectors

rainbow.math.linear.vector.subtract-negation

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

Interaction laws between native vector subtraction and negation. left - (-right) ~ left + right -(left - right) ~ right - left The proofs normalize subtraction to addition of a negation and compose vector congruence, negation involutivity, negation distributivity, commutativity, and equivalence transitivity. Native and axiom-free on D63.

Depends onmath.linear.vector.subtract-laws

vector/subtract-negate :
  (left right : List ℚ)
  → vector/equivalent (subtract) (vector/add left right)
  where subtract := vector/subtract left (vector/negate right)

vector/negate-subtract :
  (left right : List ℚ)
  → vector/equivalent (vector/negate (vector/subtract left right)) (vector/subtract right left)