Reference · Vectors

rainbow.math.linear.vector.negate-additive

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

Native vector negation distributes over native vector addition. -(left + right) ~ (-left) + (-right) Vector addition truncates to the shorter list, and both sides truncate at the same position. The cons/cons case invokes signed/negate-additive and the tail induction hypothesis. Native and axiom-free on D63.

Depends onmath.rational.signed.negate-additivemath.finite.vectormath.linear.vector.equivalence

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