Reference · Matrices

rainbow.math.linear.matrix.composable

Matricessrc/rainbow/math/linear/matrix/composable.clj1 definitions, 6 theorems

Dimension certificates for native finite matrix composition. matrix/composable left right combines the exact inner-dimension condition (every left row has the shape of right's row-count vector) with rectangularity of right. Compatibility itself forces left rectangularity, so projections recover both operand shape facts. Column-shape respects matrix equivalence, and the full composability certificate transports across equivalent operands. This is the quotient-safe precondition for later associativity. Native and axiom-free on D63.

Depends onmath.linear.matrix.multiply-shape

matrix/composable :
  (x₁ x₂ : List (List ℚ))
  → Prop

matrix/compatible-implies-rectangular :
  (rows : List (List ℚ)) (values : List ℚ)
  (rows-compatible : matrix/compatible rows values)
  → matrix/rectangular rows

matrix/composable-inner-compatible :
  (left right : List (List ℚ)) (can-compose : matrix/composable left right)
  → matrix/compatible left (matrix/column-shape right)

matrix/composable-left-rectangular :
  (left right : List (List ℚ)) (can-compose : matrix/composable left right)
  → matrix/rectangular left

matrix/composable-right-rectangular :
  (left right : List (List ℚ)) (can-compose : matrix/composable left right)
  → matrix/rectangular right

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

matrix/composable-respects-equivalence :
  (left equivalent-left right equivalent-right : List (List ℚ))
  (left-same : matrix/equivalent left equivalent-left)
  (right-same : matrix/equivalent right equivalent-right)
  (can-compose : matrix/composable left right)
  → matrix/composable equivalent-left equivalent-right