OAI/LinearAlgebra/MatrixMultiplication/FieldConstruction/InitialZeroFinish.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Tensor extraction over arbitrary fields and its asymptotic rate.

  1. abbrev OAI.MatrixMultiplication.AllFieldInitialZeroFinish.Index line 20
  2. theorem OAI.MatrixMultiplication.AllFieldInitialZeroFinish.shape_total line 24
  3. theorem OAI.MatrixMultiplication.AllFieldInitialZeroFinish.has_zero line 27
  4. theorem OAI.MatrixMultiplication.AllFieldInitialZeroFinish.canonical_axes_ne line 30
  5. def OAI.MatrixMultiplication.AllFieldInitialZeroFinish.zero line 35
  6. def OAI.MatrixMultiplication.AllFieldInitialZeroFinish.selected line 36
  7. theorem OAI.MatrixMultiplication.AllFieldInitialZeroFinish.axes_ne line 38
  8. theorem OAI.MatrixMultiplication.AllFieldInitialZeroFinish.weights_sum line 41
  9. theorem OAI.MatrixMultiplication.AllFieldInitialZeroFinish.physical_shape_eq line 45
  10. def OAI.MatrixMultiplication.AllFieldInitialZeroFinish.embed line 56
  11. theorem OAI.MatrixMultiplication.AllFieldInitialZeroFinish.coefficient line 60
  12. abbrev OAI.MatrixMultiplication.AllFieldInitialZeroFinish.RowIndex line 73
  13. abbrev OAI.MatrixMultiplication.AllFieldInitialZeroFinish.MiddleIndex line 74
  14. abbrev OAI.MatrixMultiplication.AllFieldInitialZeroFinish.ColumnIndex line 75
  15. def OAI.MatrixMultiplication.AllFieldInitialZeroFinish.factorMap line 77
  16. theorem OAI.MatrixMultiplication.AllFieldInitialZeroFinish.factor_volume line 86
  17. abbrev OAI.MatrixMultiplication.AllFieldInitialZeroFinish.RawWords line 93
  18. abbrev OAI.MatrixMultiplication.AllFieldInitialZeroFinish.Rows line 95
  19. abbrev OAI.MatrixMultiplication.AllFieldInitialZeroFinish.Middles line 96
  20. abbrev OAI.MatrixMultiplication.AllFieldInitialZeroFinish.Columns line 97
  21. def OAI.MatrixMultiplication.AllFieldInitialZeroFinish.source line 99
  22. def OAI.MatrixMultiplication.AllFieldInitialZeroFinish.finishMap line 105
  23. theorem OAI.MatrixMultiplication.AllFieldInitialZeroFinish.volume_eq line 118
  24. theorem OAI.MatrixMultiplication.AllFieldInitialZeroFinish.volume_pos line 130
  25. theorem OAI.MatrixMultiplication.AllFieldInitialZeroFinish.rows_pos line 137
  26. theorem OAI.MatrixMultiplication.AllFieldInitialZeroFinish.middles_pos line 140
  27. theorem OAI.MatrixMultiplication.AllFieldInitialZeroFinish.columns_pos line 143