Reference · Vectors

rainbow.math.linear.vector.scale-additive

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

Uniform nonnegative scaling distributes over native vector addition. scale c (left + right) ~ scale c left + scale c right Vector addition truncates to the shorter list, and both sides truncate at the same position. The cons/cons case invokes signed/scale-additive and the tail induction hypothesis. Native and axiom-free on D63.

Depends onmath.rational.signed.scale-additivemath.finite.vectormath.linear.vector.equivalence

vector/scale-additive :
  (rate : ℚ≥0) (left right : List ℚ)
  → vector/equivalent (scale) (add)
  where add := vector/add (vector/scale rate left) (vector/scale rate right)
  where scale := vector/scale rate (vector/add left right)