OAI/LinearAlgebra/MatrixMultiplication/Tensor/ComplexMatrixTensor.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Finite coefficient tensors and their algebraic transformations.

  1. def OAI.MatrixMultiplication.Foundation.Tensor.matrixCoefficients line 17
  2. theorem OAI.MatrixMultiplication.Foundation.Tensor.matrixMultiplication_eq_matrixCoefficients line 21
  3. theorem OAI.MatrixMultiplication.Foundation.Tensor.contract_matrixCoefficients line 24
  4. theorem OAI.MatrixMultiplication.Foundation.Tensor.matrixCoefficients_product line 31
  5. theorem OAI.MatrixMultiplication.Foundation.Tensor.matrixCoefficients_cyclic line 42
  6. theorem OAI.MatrixMultiplication.Foundation.Tensor.matrixCoefficients_rank_of_product line 50
  7. theorem OAI.MatrixMultiplication.Foundation.Tensor.matrixCoefficients_product_rank line 70
  8. theorem OAI.MatrixMultiplication.Foundation.Tensor.matrixCoefficients_batch_rank line 77
  9. theorem OAI.MatrixMultiplication.Foundation.Tensor.matrixCoefficients_power line 85
  10. theorem OAI.MatrixMultiplication.Foundation.Tensor.matrixCoefficients_cyclic_rank line 93