Reference · Vectors

rainbow.math.linear.vector.scale-order

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

Nonnegative-rational scaling preserves native positional vector order. left <= right -> scale c left <= scale c right The proof follows the two list shapes carried by vector/at-most. Matching components invoke signed/scale-monotone; mismatched dimensions are already false and therefore need no arithmetic. Native and axiom-free on D63.

Depends onmath.rational.signed.scale-ordermath.finite.vectormath.linear.vector.pointwise-order-laws

vector/scale-monotone :
  (rate : ℚ≥0) (left right : List ℚ) (ordered : vector/at-most left right)
  → vector/at-most (vector/scale rate left) (vector/scale rate right)

vector/scale-respects-equivalence :
  (rate : ℚ≥0) (left right : List ℚ) (same : vector/equivalent left right)
  → vector/equivalent (vector/scale rate left) (vector/scale rate right)