Reference · Matrices

rainbow.math.linear.matrix.multiply-shape

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

Unconditional output-shape laws for native matrix multiplication. matrix/vector-multiply always returns one component per matrix row, so its result has matrix/column-shape. Lifting that fact through matrix/multiply proves that product row count matches the left matrix, every output row is compatible with any other row image, and every product is rectangular—even when the total ragged/truncating semantics is used. Native and axiom-free on D63.

Depends onmath.linear.matrix.multiply

matrix/vector-multiply-column-shape :
  (rows : List (List ℚ)) (values : List ℚ)
  → vector/same-shape (matrix/vector-multiply rows values) (matrix/column-shape rows)

matrix/multiply-left-column-shape :
  (left right : List (List ℚ))
  → vector/same-shape (matrix/column-shape (matrix/multiply left right)) (matrix/column-shape left)

matrix/multiply-compatible-with-row-image :
  (left right : List (List ℚ)) (reference : List ℚ)
  → matrix/compatible (matrix/multiply left right) (multiply)
  where multiply := matrix/vector-multiply (matrix/transpose right) reference

matrix/multiply-rectangular :
  (left right : List (List ℚ))
  → matrix/rectangular (matrix/multiply left right)