Reference · Matrices

rainbow.math.linear.matrix.negate-linear

Matricessrc/rainbow/math/linear/matrix/negate_linear.clj0 definitions, 5 theorems

Negation commutes with native matrix action, transpose, and multiplication. Row-wise action negation follows from dot negation. A structural column insertion law transports pointwise negation through total transpose. These bridges prove that negating either factor negates the native matrix product, without rectangularity or compatibility premises. Native and axiom-free on D63.

Depends onmath.linear.matrix.additive-group

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

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

matrix/transpose-negate :
  (rows : List (List ℚ))
  → matrix/equivalent (matrix/transpose (matrix/negate rows)) (matrix/negate (matrix/transpose rows))

matrix/multiply-negate-left :
  (left right : List (List ℚ))
  → matrix/equivalent (multiply) (matrix/negate (matrix/multiply left right))
  where multiply := matrix/multiply (matrix/negate left) right

matrix/multiply-negate-right :
  (left right : List (List ℚ))
  → matrix/equivalent (multiply) (matrix/negate (matrix/multiply left right))
  where multiply := matrix/multiply left (matrix/negate right)