Reference · Matrices

rainbow.math.linear.matrix.equivalence-shape

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

Shape transport for length-sensitive native matrix equivalence. Componentwise vector equivalence already forces equal list length, so it implies vector/same-shape. Lifting that observation row-wise completes matrix/equivalent as an equivalence relation and proves that replacing a matrix by an equivalent one preserves compatibility and rectangularity. These are the transport laws required before shape-safe transpose and matrix composition can be exposed. Native and axiom-free on D63.

Depends onmath.linear.matrix.equivalence

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

matrix/equivalent-transitive :
  (left middle right : List (List ℚ)) (left-middle : matrix/equivalent left middle)
  (middle-right : matrix/equivalent middle right)
  → matrix/equivalent left right

matrix/equivalent-preserves-compatibility :
  (left right : List (List ℚ)) (values : List ℚ) (same : matrix/equivalent left right)
  (left-compatible : matrix/compatible left values)
  → matrix/compatible right values

matrix/equivalent-preserves-rectangularity :
  (left right : List (List ℚ)) (same : matrix/equivalent left right)
  (left-rectangular : matrix/rectangular left)
  → matrix/rectangular right