Reference · Matrices

rainbow.math.linear.matrix.transpose-shape

Matricessrc/rainbow/math/linear/matrix/transpose_shape.clj1 definitions, 7 theorems

Rectangularity laws for total native matrix transpose. matrix/column-shape maps each row of a matrix to one signed zero, yielding a vector whose length is the matrix row count. Thus vector/same-shape between an inserted vector and column-shape records the exact width precondition for matrix/prepend-column. Structural laws show insertion preserves compatibility and rectangularity under that certificate, and finally that transpose sends every rectangular matrix to a rectangular matrix. Native and axiom-free on D63.

Depends onmath.linear.matrix.transpose-equivalence

matrix/column-shape :
  (x₁ : List (List ℚ))
  → List ℚ

matrix/prepend-column-output-shape :
  (values : List ℚ) (columns : List (List ℚ))
  → vector/same-shape (matrix/column-shape (matrix/prepend-column values columns)) values

matrix/prepend-column-empty-compatible-singleton :
  (values : List ℚ) (reference : ℚ)
  → matrix/compatible (matrix/prepend-column values []) [reference]

matrix/prepend-column-empty-rectangular :
  (values : List ℚ)
  → matrix/rectangular (matrix/prepend-column values [])

matrix/prepend-column-preserves-compatibility :
  (values : List ℚ) (columns : List (List ℚ)) (reference-head : ℚ)
  (reference-column : List ℚ)
  (width : vector/same-shape values (matrix/column-shape columns))
  (columns-compatible : matrix/compatible columns reference-column)
  → matrix/compatible (matrix/prepend-column values columns) (cons)
  where cons := data/cons ℚ reference-head reference-column

matrix/prepend-column-preserves-rectangularity :
  (values : List ℚ) (columns : List (List ℚ))
  (width : vector/same-shape values (matrix/column-shape columns))
  (columns-rectangular : matrix/rectangular columns)
  → matrix/rectangular (matrix/prepend-column values columns)

matrix/transpose-cons-preserves-rectangularity :
  (row : List ℚ) (tail : List (List ℚ))
  (rows-rectangular : matrix/rectangular (data/cons (List ℚ) row tail))
  (tail-transpose-rectangular : matrix/rectangular (matrix/transpose tail))
  → matrix/rectangular (matrix/transpose (data/cons (List ℚ) row tail))

matrix/transpose-preserves-rectangularity :
  (rows : List (List ℚ)) (rows-rectangular : matrix/rectangular rows)
  → matrix/rectangular (matrix/transpose rows)