OAI/LinearAlgebra/MatrixMultiplication/Tensor/ComplexBatchCeiling.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Finite coefficient tensors and their algebraic transformations.

  1. def OAI.MatrixMultiplication.Foundation.batchCount line 10
  2. theorem OAI.MatrixMultiplication.Foundation.batchCount_zero line 12
  3. theorem OAI.MatrixMultiplication.Foundation.le_batchCount_mul line 19
  4. theorem OAI.MatrixMultiplication.Foundation.batchCount_le_iff line 27
  5. theorem OAI.MatrixMultiplication.Foundation.batchCount_mul_lt line 33
  6. theorem OAI.MatrixMultiplication.Foundation.batchCount_pos_iff line 39
  7. theorem OAI.MatrixMultiplication.Foundation.batchCount_cast_lt line 45
  8. theorem OAI.MatrixMultiplication.Foundation.batchCount_cast_le line 56
  9. theorem OAI.MatrixMultiplication.Foundation.batchCount_mul_cast_le line 60
  10. def OAI.MatrixMultiplication.Foundation.batchRank line 72
  11. theorem OAI.MatrixMultiplication.Foundation.batchRank_zero line 76
  12. theorem OAI.MatrixMultiplication.Foundation.batchRank_succ line 78
  13. theorem OAI.MatrixMultiplication.Foundation.batchRank_succ_le_affine line 81
  14. theorem OAI.MatrixMultiplication.Foundation.batchRank_pos line 87
  15. theorem OAI.MatrixMultiplication.Foundation.Tensor.RankAtMost.repeat_batch_ceiling line 100
  16. theorem OAI.MatrixMultiplication.Foundation.Tensor.RankAtMost.batch_product_ceiling line 105
  17. theorem OAI.MatrixMultiplication.Foundation.Tensor.matrixCoefficients_batch_rank_ceiling line 112