Reference · Vectors

rainbow.math.linear.vector.dot-bilinear

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

Right additivity of the native dot product, completing additive bilinearity. same-shape left right -> dot weights (left + right) ~ dot weights left + dot weights right Commute the outer dot, apply vector/dot-additive-left, then commute each resulting dot through signed addition congruence. Native and axiom-free.

Depends onmath.linear.vector.dot-additive

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