OAI/LinearAlgebra/MatrixMultiplication/FieldConstruction/ZeroFinish.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Tensor extraction over arbitrary fields and its asymptotic rate.

  1. def OAI.MatrixMultiplication.AllFieldZeroFinish.canonicalZero line 20
  2. def OAI.MatrixMultiplication.AllFieldZeroFinish.canonicalSelected line 21
  3. def OAI.MatrixMultiplication.AllFieldZeroFinish.physicalZero line 24
  4. def OAI.MatrixMultiplication.AllFieldZeroFinish.physicalSelected line 25
  5. theorem OAI.MatrixMultiplication.AllFieldZeroFinish.shape_has_zero line 27
  6. theorem OAI.MatrixMultiplication.AllFieldZeroFinish.canonicalZero_spec line 32
  7. theorem OAI.MatrixMultiplication.AllFieldZeroFinish.canonicalSelected_spec line 35
  8. theorem OAI.MatrixMultiplication.AllFieldZeroFinish.shape_total line 41
  9. theorem OAI.MatrixMultiplication.AllFieldZeroFinish.shape_total_pos line 44
  10. theorem OAI.MatrixMultiplication.AllFieldZeroFinish.axes_distinct line 48
  11. theorem OAI.MatrixMultiplication.AllFieldZeroFinish.physical_axes_distinct line 52
  12. theorem OAI.MatrixMultiplication.AllFieldZeroFinish.physical_shape line 55
  13. def OAI.MatrixMultiplication.AllFieldZeroFinish.nativeLaw line 61
  14. theorem OAI.MatrixMultiplication.AllFieldZeroFinish.selected_law line 65
  15. theorem OAI.MatrixMultiplication.AllFieldZeroFinish.zero_law line 79
  16. theorem OAI.MatrixMultiplication.AllFieldZeroFinish.remaining_law line 103
  17. def OAI.MatrixMultiplication.AllFieldZeroFinish.embed line 122
  18. theorem OAI.MatrixMultiplication.AllFieldZeroFinish.embed_window line 127
  19. theorem OAI.MatrixMultiplication.AllFieldZeroFinish.embed_mask line 168
  20. theorem OAI.MatrixMultiplication.AllFieldZeroFinish.coefficient line 183
  21. abbrev OAI.MatrixMultiplication.AllFieldZeroFinish.Row line 196
  22. abbrev OAI.MatrixMultiplication.AllFieldZeroFinish.Middle line 198
  23. abbrev OAI.MatrixMultiplication.AllFieldZeroFinish.Column line 200
  24. def OAI.MatrixMultiplication.AllFieldZeroFinish.localMap line 203
  25. theorem OAI.MatrixMultiplication.AllFieldZeroFinish.volume line 212
  26. theorem OAI.MatrixMultiplication.AllFieldZeroFinish.dimensions_pos line 217