Reference · Matrices

rainbow.math.linear.matrix.add-shape

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

Equivalence laws for matrix shape and shape preservation by addition. The structural matrix/same-shape relation is symmetric and transitive. Adding same-shaped matrices preserves the complete two-level shape of both inputs. These certificates are the shape infrastructure needed to transport addition through total transpose. Native and axiom-free on D63.

Depends onmath.linear.matrix.add

matrix/same-shape-symmetric :
  (left right : List (List ℚ)) (same : matrix/same-shape left right)
  → matrix/same-shape right left

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

matrix/add-preserves-shape :
  (left right : List (List ℚ)) (same : matrix/same-shape left right)
  → proposition/conjunction (shape₁) (shape)
  where shape := matrix/same-shape (matrix/add left right) right
  where shape₁ := matrix/same-shape (matrix/add left right) left