Reference · Matrices

rainbow.math.linear.matrix.transpose-involution

Matricessrc/rainbow/math/linear/matrix/transpose_involution.clj0 definitions, 2 theorems

Algebraic foundations for nondegenerate transpose involution. A row-list matrix cannot retain the number of rows of a nonempty zero-width matrix: matrix/transpose of rows of empty vectors is empty. Accordingly the eventual involution theorem must require positive width. The first two native lemmas prove the core valid algebra: transpose undoes insertion of a nonempty vector into empty columns, and into nonempty columns whose remaining count matches the remaining vector width. Native and axiom-free on D63.

Depends onmath.linear.matrix.transpose-shape

matrix/transpose-prepend-column-empty :
  (head : ℚ) (tail : List ℚ)
  → matrix/equivalent (matrix/transpose (column)) [data/cons ℚ head tail]
  where column := matrix/prepend-column (data/cons ℚ head tail) []

matrix/transpose-prepend-column-cons :
  (head : ℚ) (tail column : List ℚ) (columns : List (List ℚ))
  (width : vector/same-shape tail (matrix/column-shape columns))
  → matrix/equivalent (matrix/transpose (column)) (cons)
  where column := matrix/prepend-column (data/cons ℚ head tail) (data/cons (List ℚ) column columns)
  where cons := data/cons (List ℚ) (data/cons ℚ head tail) (matrix/transpose (data/cons (List ℚ) column columns))