Reference · Matrices

rainbow.math.linear.matrix.signed-scale-right

Matricessrc/rainbow/math/linear/matrix/signed_scale_right.clj0 definitions, 4 theorems

The complementary half of arbitrary signed matrix bilinearity. Scaling every row of a native matrix scales its action. Pointwise signed scaling also commutes with the total prepend-column operation, hence with total transpose even for ragged and empty matrices. Together these facts prove unrestricted homogeneity in the right factor of matrix multiplication. Native and axiom-free on D63.

Depends onmath.linear.matrix.signed-scale

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

matrix/prepend-column-signed-scale :
  (factor : ℚ) (values : List ℚ) (columns : List (List ℚ))
  → matrix/equivalent (column) (scale)
  where column := matrix/prepend-column (vector/signed-scale factor values) (matrix/signed-scale factor columns)
  where scale := matrix/signed-scale factor (matrix/prepend-column values columns)

matrix/transpose-signed-scale :
  (factor : ℚ) (rows : List (List ℚ))
  → matrix/equivalent (matrix/transpose (matrix/signed-scale factor rows)) (scale)
  where scale := matrix/signed-scale factor (matrix/transpose rows)

matrix/multiply-signed-scale-right :
  (factor : ℚ) (left right : List (List ℚ))
  → matrix/equivalent (multiply) (scale)
  where multiply := matrix/multiply left (matrix/signed-scale factor right)
  where scale := matrix/signed-scale factor (matrix/multiply left right)