Reference · Matrices

rainbow.math.linear.matrix.add

Matricessrc/rainbow/math/linear/matrix/add.clj2 definitions, 3 theorems

Length-sensitive shape, addition, and left distributivity for matrices. matrix/same-shape requires the same row count and the same length for each corresponding row. matrix/add zips rows with the existing truncating vector addition. The shape premise is exactly what makes native matrix action additive in its rows and matrix multiplication distributive in its left factor under total list semantics. Native and axiom-free on D63.

Depends onmath.linear.matrix.signed-scale-right

matrix/same-shape :
  (x₁ x₂ : List (List ℚ))
  → Prop

matrix/add :
  (x₁ x₂ : List (List ℚ))
  → List (List ℚ)

matrix/same-shape-reflexive :
  (rows : List (List ℚ))
  → matrix/same-shape rows rows

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

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