Reference · Matrices

rainbow.math.linear.matrix.linear

Matricessrc/rainbow/math/linear/matrix/linear.clj0 definitions, 3 theorems

Shape and scalar-linearity laws for native matrix-vector multiplication. matrix/vector-multiply-output-shape matrix/vector-multiply-negate matrix/vector-multiply-scale The output length is determined solely by the number of rows, even for a ragged matrix. Row-wise dot-product laws then show that the matrix action commutes with vector negation and nonnegative-rational scaling. Native and axiom-free on D63.

Depends onmath.finite.matrix

matrix/vector-multiply-output-shape :
  (rows : List (List ℚ)) (left right : List ℚ)
  → vector/same-shape (matrix/vector-multiply rows left) (matrix/vector-multiply rows right)

matrix/vector-multiply-negate :
  (rows : List (List ℚ)) (values : List ℚ)
  → vector/equivalent (multiply) (vector/negate (matrix/vector-multiply rows values))
  where multiply := matrix/vector-multiply rows (vector/negate values)

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