Reference · Matrices

rainbow.math.linear.matrix.add-right

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

Transpose additivity and right distributivity for native matrices. A joint induction proves that total transpose preserves matrix/same-shape and commutes with matrix/add. Row-wise action additivity then yields matrix multiplication distributivity in its right factor. The only premise is the exact two-level shape equality required by truncating addition; ragged and empty matrices remain supported. Native and axiom-free on D63.

Depends onmath.linear.matrix.prepend-add

matrix/transpose-additive-with-shape :
  (left right : List (List ℚ)) (shape : matrix/same-shape left right)
  → proposition/conjunction (shape) (equivalent)
  where equivalent := matrix/equivalent (matrix/transpose (matrix/add left right)) (matrix/add (matrix/transpose left) (matrix/transpose right))
  where shape := matrix/same-shape (matrix/transpose left) (matrix/transpose right)

matrix/transpose-preserves-same-shape :
  (left right : List (List ℚ)) (shape : matrix/same-shape left right)
  → matrix/same-shape (matrix/transpose left) (matrix/transpose right)

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

matrix/multiply-additive-right :
  (left right offset : List (List ℚ)) (shape : matrix/same-shape right offset)
  → matrix/equivalent (multiply) (add)
  where add := matrix/add (matrix/multiply left right) (matrix/multiply left offset)
  where multiply := matrix/multiply left (matrix/add right offset)