Reference · Matrices

rainbow.math.linear.matrix.transpose

Matrices src/rainbow/math/linear/matrix/transpose.clj2 definitions, 5 theorems

Total transpose primitives for row-major finite signed matrices. matrix/prepend-column inserts a vector as the new first component of each existing column. Its recursion is anchored to the vector: missing columns become singleton columns and surplus columns are dropped. Folding that primitive from the bottom row upward defines matrix/transpose. Rectangular matrices therefore receive ordinary transpose semantics, while ragged input still has deterministic total behavior. The constructor laws form the reduction API for later shape, involution, and matrix-composition proofs. Native and axiom-free on D63.

Depends onmath.linear.matrix.equivalence

matrix/prepend-column

DefinitionSource, line 48

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

List = data/Listℚ = signed/SignedRational

matrix/transpose

DefinitionSource, line 85

matrix/transpose :
  (x₁ : List (List ℚ))
  → List (List ℚ)

List = data/Listℚ = signed/SignedRational

matrix/prepend-column-empty-vector

TheoremFor all inputsNo axiomsSource, line 100

matrix/prepend-column-empty-vector :
  (columns : List (List ℚ))
  → matrix/equivalent (matrix/prepend-column [] columns) []

List = data/Listℚ = signed/SignedRational

matrix/prepend-column-cons-empty

TheoremFor all inputsNo axiomsSource, line 114

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

List = data/Listℚ = signed/SignedRational

matrix/prepend-column-cons-cons

TheoremFor all inputsNo axiomsSource, line 132

matrix/prepend-column-cons-cons :
  (head : ℚ) (tail column : List ℚ) (columns : List (List ℚ))
  → matrix/equivalent (column) (cons)
  where column := matrix/prepend-column (data/cons ℚ head tail) (data/cons (List ℚ) column columns)
  where cons := data/cons (List ℚ) (data/cons ℚ head column) (matrix/prepend-column tail columns)

List = data/Listℚ = signed/SignedRational

matrix/transpose-empty

TheoremWorked exampleNo axiomsSource, line 154

matrix/transpose-empty :
  → matrix/equivalent (matrix/transpose []) []

matrix/transpose-cons

TheoremFor all inputsNo axiomsSource, line 161

matrix/transpose-cons :
  (row : List ℚ) (tail : List (List ℚ))
  → matrix/equivalent (matrix/transpose (data/cons (List ℚ) row tail)) (column)
  where column := matrix/prepend-column row (matrix/transpose tail)

List = data/Listℚ = signed/SignedRational