OAI/LinearAlgebra/MatrixMultiplication/CoppersmithWinograd/ComplexCWOriginalWords.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

Coppersmith–Winograd tensors, tensor powers and local restrictions.

  1. abbrev OAI.MatrixMultiplication.Foundation.CWOriginalWords.OriginalComponent line 14
  2. theorem OAI.MatrixMultiplication.Foundation.CWOriginalWords.originalComponent_card line 17
  3. def OAI.MatrixMultiplication.Foundation.CWOriginalWords.OriginalComponent.x line 22
  4. def OAI.MatrixMultiplication.Foundation.CWOriginalWords.OriginalComponent.y line 23
  5. def OAI.MatrixMultiplication.Foundation.CWOriginalWords.OriginalComponent.z line 24
  6. theorem OAI.MatrixMultiplication.Foundation.CWOriginalWords.OriginalComponent.sum_eq_two line 26
  7. theorem OAI.MatrixMultiplication.Foundation.CWOriginalWords.OriginalComponent.ext line 29
  8. theorem OAI.MatrixMultiplication.Foundation.CWOriginalWords.OriginalComponent.eq_of_xy line 34
  9. theorem OAI.MatrixMultiplication.Foundation.CWOriginalWords.OriginalComponent.eq_of_xz line 42
  10. theorem OAI.MatrixMultiplication.Foundation.CWOriginalWords.OriginalComponent.eq_of_yz line 50
  11. theorem OAI.MatrixMultiplication.Foundation.CWOriginalWords.OriginalComponent.coefficient line 58
  12. def OAI.MatrixMultiplication.Foundation.CWOriginalWords.OriginalComponent.coordinate line 62
  13. theorem OAI.MatrixMultiplication.Foundation.CWOriginalWords.OriginalComponent.coordinate_sum line 67
  14. theorem OAI.MatrixMultiplication.Foundation.CWOriginalWords.OriginalComponent.coordinate_injective line 71
  15. def OAI.MatrixMultiplication.Foundation.CWOriginalWords.OriginalComponent.permute line 75
  16. theorem OAI.MatrixMultiplication.Foundation.CWOriginalWords.OriginalComponent.coordinate_permute line 80
  17. theorem OAI.MatrixMultiplication.Foundation.CWOriginalWords.OriginalComponent.permute_injective line 85
  18. theorem OAI.MatrixMultiplication.Foundation.CWOriginalWords.tensor_ne_zero_iff line 94
  19. def OAI.MatrixMultiplication.Foundation.CWOriginalWords.decodeComponent line 98
  20. theorem OAI.MatrixMultiplication.Foundation.CWOriginalWords.decodeComponent_coordinates line 102
  21. def OAI.MatrixMultiplication.Foundation.CWOriginalWords.xWord line 112
  22. def OAI.MatrixMultiplication.Foundation.CWOriginalWords.yWord line 113
  23. def OAI.MatrixMultiplication.Foundation.CWOriginalWords.zWord line 114
  24. def OAI.MatrixMultiplication.Foundation.CWOriginalWords.originalWords line 116
  25. def OAI.MatrixMultiplication.Foundation.CWOriginalWords.decodeWord line 120
  26. theorem OAI.MatrixMultiplication.Foundation.CWOriginalWords.decodeWord_originalWords line 123
  27. theorem OAI.MatrixMultiplication.Foundation.CWOriginalWords.originalWords_decodeWord_of_support line 128
  28. theorem OAI.MatrixMultiplication.Foundation.CWOriginalWords.decodeWord_eq_iff_of_support line 143
  29. theorem OAI.MatrixMultiplication.Foundation.CWOriginalWords.originalWords_injective line 157
  30. theorem OAI.MatrixMultiplication.Foundation.CWOriginalWords.xyWords_injective line 165
  31. theorem OAI.MatrixMultiplication.Foundation.CWOriginalWords.xzWords_injective line 172
  32. theorem OAI.MatrixMultiplication.Foundation.CWOriginalWords.yzWords_injective line 179
  33. def OAI.MatrixMultiplication.Foundation.CWOriginalWords.permuteWord line 186
  34. theorem OAI.MatrixMultiplication.Foundation.CWOriginalWords.permuteWord_injective line 190
  35. theorem OAI.MatrixMultiplication.Foundation.CWOriginalWords.oriented_originalWords_injective line 196
  36. def OAI.MatrixMultiplication.Foundation.CWOriginalWords.siteTensor line 202
  37. theorem OAI.MatrixMultiplication.Foundation.CWOriginalWords.siteTensor_originalWords line 205
  38. theorem OAI.MatrixMultiplication.Foundation.CWOriginalWords.siteTensor_originalWords_ne_zero line 210
  39. theorem OAI.MatrixMultiplication.Foundation.CWOriginalWords.siteTensor_oriented_originalWords line 215
  40. theorem OAI.MatrixMultiplication.Foundation.CWOriginalWords.siteTensor_ne_zero_iff line 221
  41. def OAI.MatrixMultiplication.Foundation.CWOriginalWords.supportedWordEquiv line 226
  42. theorem OAI.MatrixMultiplication.Foundation.CWOriginalWords.word_card line 244
  43. theorem OAI.MatrixMultiplication.Foundation.CWOriginalWords.siteTensor_eq_power line 250
  44. theorem OAI.MatrixMultiplication.Foundation.CWOriginalWords.power_originalWords line 258
  45. theorem OAI.MatrixMultiplication.Foundation.CWOriginalWords.power_originalWords_ne_zero line 262