Reference · Vectors

rainbow.math.linear.vector.dot-negate

Vectorssrc/rainbow/math/linear/vector/dot_negate.clj0 definitions, 5 theorems

Negation laws for signed multiplication and the native vector dot product. signed/negate-zero signed/multiply-negate-left signed/multiply-negate-right vector/dot-negate-left vector/dot-negate-right The scalar product laws are unfolded Grothendieck-pair ring identities. The left dot law is a native List induction, while the right law follows from dot commutativity and quotient-safe negation congruence. No shape hypothesis is needed because componentwise negation preserves every list position.

Depends onmath.linear.vector.dot-bilinearmath.rational.nnrat.ring

signed/negate-zero :
  → signed/negate 0 = 0

signed/multiply-negate-left :
  (left right : ℚ)
  → signed/negate left · right = signed/negate (left · right)

signed/multiply-negate-right :
  (left right : ℚ)
  → left · signed/negate right = signed/negate (left · right)

vector/dot-negate-left :
  (values weights : List ℚ)
  → vector/dot (vector/negate values) weights = signed/negate (vector/dot values weights)

vector/dot-negate-right :
  (values weights : List ℚ)
  → vector/dot values (vector/negate weights) = signed/negate (vector/dot values weights)