OAI/LinearAlgebra/MatrixMultiplication/Tensor/ComplexPairingMatrixTensor.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Finite coefficient tensors and their algebraic transformations.

  1. def OAI.MatrixMultiplication.Foundation.Tensor.dotPairingMatrixX line 13
  2. def OAI.MatrixMultiplication.Foundation.Tensor.dotPairingMatrixY line 19
  3. def OAI.MatrixMultiplication.Foundation.Tensor.dotPairingMatrixZ line 25
  4. theorem OAI.MatrixMultiplication.Foundation.Tensor.dotPairing_matrixCoefficients line 31
  5. theorem OAI.MatrixMultiplication.Foundation.Tensor.matrixCoefficients_rank_of_dotPairing line 51
  6. theorem OAI.MatrixMultiplication.Foundation.Tensor.matrixCoefficients_borderRank_of_dotPairing line 58
  7. def OAI.MatrixMultiplication.Foundation.Tensor.pairingTriple line 66
  8. def OAI.MatrixMultiplication.Foundation.Tensor.pairingTripleMatrixX line 71
  9. def OAI.MatrixMultiplication.Foundation.Tensor.pairingTripleMatrixY line 77
  10. def OAI.MatrixMultiplication.Foundation.Tensor.pairingTripleMatrixZ line 83
  11. theorem OAI.MatrixMultiplication.Foundation.Tensor.pairingTriple_matrixCoefficients line 91
  12. theorem OAI.MatrixMultiplication.Foundation.Tensor.matrixCoefficients_rank_of_pairingTriple line 104
  13. theorem OAI.MatrixMultiplication.Foundation.Tensor.matrixCoefficients_borderRank_of_pairingTriple line 112
  14. theorem OAI.MatrixMultiplication.Foundation.Tensor.matrixCoefficients_directSum_rank_of_pairingTriple line 120
  15. theorem OAI.MatrixMultiplication.Foundation.Tensor.matrixCoefficients_directSum_borderRank_of_pairingTriple line 128