Reference · Vectors

rainbow.math.linear.vector.scale-subtract

Vectorssrc/rainbow/math/linear/vector/scale_subtract.clj0 definitions, 2 theorems

Uniform nonnegative scaling commutes with negation and subtraction. scale rate (-values) ~ -(scale rate values) scale rate (left - right) ~ scale rate left - scale rate right At each scalar head, scaling a negated Grothendieck pair and negating a scaled pair are definitionally the same pair. Subtraction distribution then composes this result with vector/scale-additive. Native and axiom-free on D63.

Depends onmath.linear.vector.add-reorder

vector/scale-negate :
  (rate : ℚ≥0) (values : List ℚ)
  → vector/equivalent (scale) (vector/negate (vector/scale rate values))
  where scale := vector/scale rate (vector/negate values)

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