rainbow.math.linear.vector.scale-composition

Vectors src/rainbow/math/linear/vector/scale_composition.clj0 definitions, 1 theorems

Composition of uniform nonnegative scaling on native signed vectors. scale outer (scale inner values) ~ scale (outer * inner) values The proof maps signed/scale-composition over the list. Native and axiom-free on D63.

Depends onmath.rational.signed.scale-composition math.finite.vector math.linear.vector.equivalence

vector/scale-composition

TheoremFor all inputsNo axiomsSource, line 45

vector/scale-composition :
  (outer inner : ℚ≥0) (values : List ℚ)
  → vector/equivalent (scale) (vector/scale (outer · inner) values)
  where scale := vector/scale outer (vector/scale inner values)

List = data/List· = nnrat/multiplyℚ = signed/SignedRationalℚ≥0 = nnrat/NonnegativeRational