OAI/LinearAlgebra/MatrixMultiplication/Tensor/ComplexExecutionPairingBudget.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

Finite coefficient tensors and their algebraic transformations.

  1. structure OAI.MatrixMultiplication.Foundation.ExecutionPairingBudget.MatrixCoordinates line 17
  2. def OAI.MatrixMultiplication.Foundation.ExecutionPairingBudget.MatrixCoordinates.volume line 29
  3. def OAI.MatrixMultiplication.Foundation.ExecutionPairingBudget.MatrixCoordinates.Positive line 32
  4. def OAI.MatrixMultiplication.Foundation.ExecutionPairingBudget.MatrixCoordinates.tensor line 35
  5. theorem OAI.MatrixMultiplication.Foundation.ExecutionPairingBudget.MatrixCoordinates.left_card line 39
  6. theorem OAI.MatrixMultiplication.Foundation.ExecutionPairingBudget.MatrixCoordinates.middle_card line 43
  7. theorem OAI.MatrixMultiplication.Foundation.ExecutionPairingBudget.MatrixCoordinates.right_card line 47
  8. def OAI.MatrixMultiplication.Foundation.ExecutionPairingBudget.MatrixCoordinates.standard line 51
  9. theorem OAI.MatrixMultiplication.Foundation.ExecutionPairingBudget.MatrixCoordinates.standard_volume line 60
  10. theorem OAI.MatrixMultiplication.Foundation.ExecutionPairingBudget.MatrixCoordinates.standard_tensor line 62
  11. def OAI.MatrixMultiplication.Foundation.ExecutionPairingBudget.MatrixCoordinates.scalar line 65
  12. theorem OAI.MatrixMultiplication.Foundation.ExecutionPairingBudget.MatrixCoordinates.scalar_volume line 73
  13. theorem OAI.MatrixMultiplication.Foundation.ExecutionPairingBudget.MatrixCoordinates.scalar_positive line 75
  14. theorem OAI.MatrixMultiplication.Foundation.ExecutionPairingBudget.MatrixCoordinates.scalar_tensor line 78
  15. def OAI.MatrixMultiplication.Foundation.ExecutionPairingBudget.MatrixCoordinates.pairProductEquiv line 82
  16. theorem OAI.MatrixMultiplication.Foundation.ExecutionPairingBudget.MatrixCoordinates.pairProductEquiv_apply line 87
  17. def OAI.MatrixMultiplication.Foundation.ExecutionPairingBudget.MatrixCoordinates.product line 92
  18. theorem OAI.MatrixMultiplication.Foundation.ExecutionPairingBudget.MatrixCoordinates.product_volume line 104
  19. theorem OAI.MatrixMultiplication.Foundation.ExecutionPairingBudget.MatrixCoordinates.product_positive line 110
  20. theorem OAI.MatrixMultiplication.Foundation.ExecutionPairingBudget.MatrixCoordinates.product_tensor line 116
  21. def OAI.MatrixMultiplication.Foundation.ExecutionPairingBudget.MatrixCoordinates.bankIndexEquiv line 143
  22. def OAI.MatrixMultiplication.Foundation.ExecutionPairingBudget.MatrixCoordinates.bank line 147
  23. theorem OAI.MatrixMultiplication.Foundation.ExecutionPairingBudget.MatrixCoordinates.bank_volume line 165
  24. theorem OAI.MatrixMultiplication.Foundation.ExecutionPairingBudget.MatrixCoordinates.bank_positive line 169
  25. theorem OAI.MatrixMultiplication.Foundation.ExecutionPairingBudget.MatrixCoordinates.bank_tensor line 175
  26. theorem OAI.MatrixMultiplication.Foundation.ExecutionPairingBudget.MatrixCoordinates.bank_budget line 201
  27. theorem OAI.MatrixMultiplication.Foundation.ExecutionPairingBudget.step_budget line 220
  28. theorem OAI.MatrixMultiplication.Foundation.ExecutionPairingBudget.initial_budget line 232
  29. def OAI.MatrixMultiplication.Foundation.ExecutionPairingBudget.primitiveBankCoordinates line 257
  30. theorem OAI.MatrixMultiplication.Foundation.ExecutionPairingBudget.primitive_bank_positive line 264
  31. theorem OAI.MatrixMultiplication.Foundation.ExecutionPairingBudget.admissible_bank_budget line 268