Reference · Matrices

rainbow.math.linear.matrix.transpose-multiply

Matricessrc/rainbow/math/linear/matrix/transpose_multiply.clj1 definitions, 4 theorems

Transpose/product structure for nonempty native finite matrices. matrix/column-action maps a matrix action over an explicit list of columns. For a nonempty left operand, transposing a native product is equivalent to applying the left matrix to every transposed right column. Nonemptiness is exact: transposing a zero-row matrix loses the number of zero-width rows. A companion theorem certifies that every column of a rectangular matrix has its row-count shape. Native and axiom-free on D63.

Depends onmath.linear.matrix.action-associative

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

matrix/transpose-compatible-column-shape :
  (rows : List (List ℚ)) (rows-rectangular : matrix/rectangular rows)
  → matrix/compatible (matrix/transpose rows) (matrix/column-shape rows)

matrix/prepend-column-action-empty :
  (row : List ℚ) (columns : List (List ℚ))
  → matrix/equivalent (column) (matrix/column-action [row] columns)
  where column := matrix/prepend-column (matrix/vector-multiply columns row) []

matrix/prepend-column-column-action :
  (row : List ℚ) (tail columns : List (List ℚ))
  → matrix/equivalent (column) (action)
  where action := matrix/column-action (data/cons (List ℚ) row tail) columns
  where column := matrix/prepend-column (matrix/vector-multiply columns row) (matrix/column-action tail columns)

matrix/transpose-multiply-nonempty-left :
  (row : List ℚ) (tail right : List (List ℚ))
  → matrix/equivalent (matrix/transpose (multiply)) (action)
  where action := matrix/column-action (data/cons (List ℚ) row tail) (matrix/transpose right)
  where multiply := matrix/multiply (data/cons (List ℚ) row tail) right