Reference · Vectors

rainbow.math.linear.vector.dot-zero-laws

Vectorssrc/rainbow/math/linear/vector/dot_zero_laws.clj0 definitions, 4 theorems

Zero laws for the native dot product and exact squared norm. vector/dot-zero-like-left vector/dot-zero-like-right norm/norm-squared-zero-like norm/is-norm-zero-like `vector/zero-like` preserves the input list shape while replacing every component by signed zero. A native List induction proves its dot product is zero against arbitrary weights; commutativity supplies the other side. The squared-norm and exact-zero-witness laws are immediate corollaries.

Depends onmath.linear.vector.dot-subtractmath.linear.vector.norm

vector/dot-zero-like-left :
  (values weights : List ℚ)
  → vector/dot (vector/zero-like values) weights = 0

vector/dot-zero-like-right :
  (weights values : List ℚ)
  → vector/dot weights (vector/zero-like values) = 0

norm/norm-squared-zero-like :
  (values : List ℚ)
  → norm/norm-squared (vector/zero-like values) = 0

norm/is-norm-zero-like :
  (values : List ℚ)
  → norm/is-norm (vector/zero-like values) 0