Reference · Matrices

rainbow.math.linear.matrix.transpose-equivalence

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

Congruence laws for total native matrix transpose. matrix/prepend-column respects vector equivalence and matrix equivalence separately, then jointly by transitivity. Structural row induction lifts the joint law to matrix/transpose. Consequently transpose is well-defined on the quotient represented by matrix/equivalent, including the explicit total semantics for ragged matrices. Native and axiom-free on D63.

Depends onmath.linear.matrix.transpose

matrix/prepend-column-respects-vector-equivalence :
  (left right : List ℚ) (columns : List (List ℚ)) (same : vector/equivalent left right)
  → matrix/equivalent (matrix/prepend-column left columns) (matrix/prepend-column right columns)

matrix/prepend-column-respects-matrix-equivalence :
  (values : List ℚ) (left right : List (List ℚ)) (same : matrix/equivalent left right)
  → matrix/equivalent (matrix/prepend-column values left) (matrix/prepend-column values right)

matrix/prepend-column-respects-equivalence :
  (left-values right-values : List ℚ) (left-columns right-columns : List (List ℚ))
  (values-same : vector/equivalent left-values right-values)
  (columns-same : matrix/equivalent left-columns right-columns)
  → matrix/equivalent (column₁) (column)
  where column := matrix/prepend-column right-values right-columns
  where column₁ := matrix/prepend-column left-values left-columns

matrix/transpose-respects-equivalence :
  (left right : List (List ℚ)) (same : matrix/equivalent left right)
  → matrix/equivalent (matrix/transpose left) (matrix/transpose right)