OAI/LinearAlgebra/MatrixMultiplication/Tensor/ComplexTensorBatching.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Finite coefficient tensors and their algebraic transformations.

  1. def OAI.MatrixMultiplication.Foundation.Tensor.diagonal line 14
  2. theorem OAI.MatrixMultiplication.Foundation.Tensor.diagonal_rankAtMost line 17
  3. theorem OAI.MatrixMultiplication.Foundation.Tensor.RankAtMost.repeat_batch line 28
  4. theorem OAI.MatrixMultiplication.Foundation.Tensor.RankAtMost.batch_substitute line 66
  5. theorem OAI.MatrixMultiplication.Foundation.Tensor.RankAtMost.batch_product line 87