Reference · Matrices

rainbow.math.linear.matrix.transpose-multiply-reverse

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

Transpose reverses native matrix multiplication at positive width. A rectangular matrix with an explicitly nonempty first row is recovered by double transpose. Mapping its action over columns is therefore equivalent to multiplying those columns by its transpose; composing that fact with the nonempty-left transpose/product bridge yields transpose (B*C) ~ transpose C * transpose B. No premise on C is required. Native and axiom-free on D63.

Depends onmath.linear.matrix.transpose-multiplymath.linear.matrix.transpose-involution-positive

matrix/column-action-to-transpose-product :
  (head : ℚ) (row-tail : List ℚ) (tail columns : List (List ℚ))
  (rows-rectangular : matrix/rectangular (data/cons (List ℚ) (data/cons ℚ head row-tail) tail))
  → matrix/equivalent (action) (multiply)
  where action := matrix/column-action (data/cons (List ℚ) (data/cons ℚ head row-tail) tail) columns
  where multiply := matrix/multiply columns (matrix/transpose (data/cons (List ℚ) (data/cons ℚ head row-tail) tail))

matrix/transpose-multiply-reverses-positive-width :
  (head : ℚ) (row-tail : List ℚ) (tail right : List (List ℚ))
  (rows-rectangular : matrix/rectangular (data/cons (List ℚ) (data/cons ℚ head row-tail) tail))
  → matrix/equivalent (matrix/transpose (multiply₁)) (multiply)
  where multiply := matrix/multiply (matrix/transpose right) (matrix/transpose (data/cons (List ℚ) (data/cons ℚ head row-tail) tail))
  where multiply₁ := matrix/multiply (data/cons (List ℚ) (data/cons ℚ head row-tail) tail) right