Reference · Vectors

rainbow.math.linear.vector.dot-congruence

Vectorssrc/rainbow/math/linear/vector/dot_congruence.clj0 definitions, 3 theorems

Quotient-safe congruence of the native vector dot product. vector/dot-left-respects-equivalence vector/dot-right-respects-equivalence vector/dot-respects-equivalence The left theorem is a structural induction over two equivalent vectors and an arbitrary weight list. Head products transport through signed multiplication congruence and tails through the induction hypothesis. Dot commutativity derives the right theorem; transitivity composes both sides.

Depends onmath.linear.vector.dot-subtract

vector/dot-left-respects-equivalence :
  (left left-prime weights : List ℚ) (same : vector/equivalent left left-prime)
  → vector/dot left weights = vector/dot left-prime weights

vector/dot-right-respects-equivalence :
  (weights left right : List ℚ) (same : vector/equivalent left right)
  → vector/dot weights left = vector/dot weights right

vector/dot-respects-equivalence :
  (left left-prime right right-prime : List ℚ)
  (left-same : vector/equivalent left left-prime)
  (right-same : vector/equivalent right right-prime)
  → vector/dot left right = vector/dot left-prime right-prime