Reference · Matrices

rainbow.math.linear.matrix.subtract-linear

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

Subtraction commutes with native matrix action, transpose, and products. Same-shaped subtraction is addition of a same-shaped negation. Reusing that shape certificate, additive bilinearity and negation linearity compose into action, transpose, and two-sided product subtraction laws. Native and axiom-free on D63.

Depends onmath.linear.matrix.negate-linear

matrix/vector-multiply-subtract-rows :
  (left right : List (List ℚ)) (values : List ℚ) (shape : matrix/same-shape left right)
  → vector/equivalent (multiply) (subtract)
  where multiply := matrix/vector-multiply (matrix/subtract left right) values
  where subtract := vector/subtract (matrix/vector-multiply left values) (matrix/vector-multiply right values)

matrix/transpose-subtract :
  (left right : List (List ℚ)) (shape : matrix/same-shape left right)
  → matrix/equivalent (matrix/transpose (matrix/subtract left right)) (subtract)
  where subtract := matrix/subtract (matrix/transpose left) (matrix/transpose right)

matrix/multiply-subtract-left :
  (left right factor : List (List ℚ)) (shape : matrix/same-shape left right)
  → matrix/equivalent (multiply) (subtract)
  where multiply := matrix/multiply (matrix/subtract left right) factor
  where subtract := matrix/subtract (matrix/multiply left factor) (matrix/multiply right factor)

matrix/multiply-subtract-right :
  (factor left right : List (List ℚ)) (shape : matrix/same-shape left right)
  → matrix/equivalent (multiply) (subtract)
  where multiply := matrix/multiply factor (matrix/subtract left right)
  where subtract := matrix/subtract (matrix/multiply factor left) (matrix/multiply factor right)