rainbow.math.linear.matrix.composable-transpose

Matrices src/rainbow/math/linear/matrix/composable_transpose.clj0 definitions, 1 theorems

Composable native matrix pairs reverse under transpose. If a nonempty matrix A composes with B, then transpose B composes with transpose A. Nonemptiness supplies A's row width as the row count of its transpose; zero-width rows remain valid. Native and axiom-free on D63.

Depends onmath.linear.matrix.transpose-multiply-reverse

matrix/composable-transpose-reverse-nonempty-left

TheoremFor all inputsNo axiomsSource, line 46

matrix/composable-transpose-reverse-nonempty-left :
  (left-head : List ℚ) (left-tail right : List (List ℚ))
  (can-compose : matrix/composable (data/cons (List ℚ) left-head left-tail) right)
  → matrix/composable (matrix/transpose right) (matrix/transpose (data/cons (List ℚ) left-head left-tail))

List = data/Listℚ = signed/SignedRational