Reference · Matrices

rainbow.math.linear.matrix.composable-multiply

Matricessrc/rainbow/math/linear/matrix/composable_multiply.clj0 definitions, 3 theorems

Closure of matrix composability under native multiplication bracketings. Row count of B*C equals row count of B, and B*C is always rectangular, so A composable B implies A composable (B*C). Conversely, when B is explicitly nonempty, B composable C fixes B's column width to C's row count; output-shape laws then show (A*B) composable C. The combined theorem certifies both sides of an associative triple without claiming their values equal yet. Native and axiom-free on D63.

Depends onmath.linear.matrix.composable

matrix/composable-with-product-right :
  (left middle right : List (List ℚ))
  (left-middle-composable : matrix/composable left middle)
  → matrix/composable left (matrix/multiply middle right)

matrix/product-left-composable :
  (left : List (List ℚ)) (middle-head : List ℚ) (middle-tail right : List (List ℚ))
  (middle-right-composable : matrix/composable (data/cons (List ℚ) middle-head middle-tail) right)
  → matrix/composable (multiply) right
  where multiply := matrix/multiply left (data/cons (List ℚ) middle-head middle-tail)

matrix/composable-bracketings :
  (left : List (List ℚ)) (middle-head : List ℚ) (middle-tail right : List (List ℚ))
  (left-middle-composable : matrix/composable left (data/cons (List ℚ) middle-head middle-tail))
  (middle-right-composable : matrix/composable (data/cons (List ℚ) middle-head middle-tail) right)
  → proposition/conjunction (composable₁) (composable)
  where composable := matrix/composable left (matrix/multiply (data/cons (List ℚ) middle-head middle-tail) right)
  where composable₁ := matrix/composable (matrix/multiply left (data/cons (List ℚ) middle-head middle-tail)) right