Reference · Vectors

rainbow.math.linear.vector.dot-additive

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

Additivity of the native dot product in its first vector argument. same-shape left right -> dot (left + right) weights ~ dot left weights + dot right weights The shape premise is necessary because vector/add is a truncating zip. A native two-list induction eliminates mismatched inputs; the cons/cons case splits on weights and combines signed multiplication distributivity, the tail induction hypothesis, and signed four-term reordering.

Depends onmath.linear.vector.shape-addmath.rational.signed.multiply

vector/dot-additive-left :
  (left right weights : List ℚ) (same : vector/same-shape left right)
  → vector/dot (vector/add left right) weights = vector/dot left weights + vector/dot right weights