OAI/LinearAlgebra/MatrixMultiplication/Tensor/BaseTensors.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

Finite coefficient tensors and their algebraic transformations.

  1. def OAI.MatrixMultiplication.BaseTwo.tensor line 16
  2. def OAI.MatrixMultiplication.BaseTwo.flagB line 19
  3. def OAI.MatrixMultiplication.BaseTwo.flagA line 20
  4. def OAI.MatrixMultiplication.BaseTwo.flagC line 21
  5. theorem OAI.MatrixMultiplication.BaseTwo.support_iff line 23
  6. theorem OAI.MatrixMultiplication.BaseTwo.one_hot line 29
  7. theorem OAI.MatrixMultiplication.BaseTwo.conditionalB line 36
  8. theorem OAI.MatrixMultiplication.BaseTwo.conditionalA line 40
  9. theorem OAI.MatrixMultiplication.BaseTwo.conditionalC line 44
  10. def OAI.MatrixMultiplication.BaseTwo.point line 48
  11. theorem OAI.MatrixMultiplication.BaseTwo.point_injective line 53
  12. theorem OAI.MatrixMultiplication.BaseTwo.point_supported line 58
  13. theorem OAI.MatrixMultiplication.BaseTwo.support_enumeration line 62
  14. theorem OAI.MatrixMultiplication.BaseTwo.tensor_eq_sum line 74
  15. theorem OAI.MatrixMultiplication.BaseTwo.color_masses line 80
  16. def OAI.MatrixMultiplication.BaseThree.tensor line 91
  17. def OAI.MatrixMultiplication.BaseThree.flagB line 93
  18. def OAI.MatrixMultiplication.BaseThree.flagA line 94
  19. def OAI.MatrixMultiplication.BaseThree.flagC line 95
  20. theorem OAI.MatrixMultiplication.BaseThree.support_iff line 97
  21. theorem OAI.MatrixMultiplication.BaseThree.one_hot line 105
  22. theorem OAI.MatrixMultiplication.BaseThree.conditionalA line 114
  23. theorem OAI.MatrixMultiplication.BaseThree.conditionalB line 120
  24. theorem OAI.MatrixMultiplication.BaseThree.conditionalC line 126
  25. theorem OAI.MatrixMultiplication.BaseThree.readableA line 131
  26. theorem OAI.MatrixMultiplication.BaseThree.readableB line 136
  27. def OAI.MatrixMultiplication.BaseThree.point line 141
  28. theorem OAI.MatrixMultiplication.BaseThree.point_injective line 148
  29. theorem OAI.MatrixMultiplication.BaseThree.point_supported line 153
  30. theorem OAI.MatrixMultiplication.BaseThree.support_enumeration line 157
  31. theorem OAI.MatrixMultiplication.BaseThree.tensor_eq_sum line 172
  32. theorem OAI.MatrixMultiplication.BaseThree.color_masses line 179