Reference · Matrices

rainbow.math.linear.matrix.multiply

Matricessrc/rainbow/math/linear/matrix/multiply.clj1 definitions, 5 theorems

Native matrix multiplication for row-major finite signed matrices. matrix/multiply left right maps each left row through matrix/vector-multiply against transpose right, so each result component is the exact dot product with a right column. The operation is total under the established ragged semantics and agrees with ordinary matrix multiplication on compatible rectangular inputs. Constructor and two-sided quotient congruence laws are native and axiom-free on D63.

Depends onmath.linear.matrix.transpose-equivalence

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

matrix/multiply-empty-left :
  (right : List (List ℚ))
  → matrix/equivalent (matrix/multiply [] right) []

matrix/multiply-cons-left :
  (row : List ℚ) (tail right : List (List ℚ))
  → matrix/equivalent (multiply) (cons)
  where cons := data/cons (List ℚ) (matrix/vector-multiply (matrix/transpose right) row) (matrix/multiply tail right)
  where multiply := matrix/multiply (data/cons (List ℚ) row tail) right

matrix/multiply-respects-left-equivalence :
  (left equivalent-left right : List (List ℚ))
  (same : matrix/equivalent left equivalent-left)
  → matrix/equivalent (matrix/multiply left right) (matrix/multiply equivalent-left right)

matrix/multiply-respects-right-equivalence :
  (left right equivalent-right : List (List ℚ))
  (same : matrix/equivalent right equivalent-right)
  → matrix/equivalent (matrix/multiply left right) (matrix/multiply left equivalent-right)

matrix/multiply-respects-equivalence :
  (left equivalent-left right equivalent-right : List (List ℚ))
  (left-same : matrix/equivalent left equivalent-left)
  (right-same : matrix/equivalent right equivalent-right)
  → matrix/equivalent (matrix/multiply left right) (multiply)
  where multiply := matrix/multiply equivalent-left equivalent-right