OAI/LinearAlgebra/MatrixFields/Construction/ZeroFinish.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldZeroWords.length line 21
  2. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldZeroWords.shape line 22
  3. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldZeroWords.statistic line 24
  4. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldZeroWords.complement line 28
  5. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldZeroWords.statistic_complement line 32
  6. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldZeroWords.words line 38
  7. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldZeroWords.words_injective line 48
  8. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldZeroWords.repeat_ratio line 60
  9. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldZeroWords.exact_window_reindex line 68
  10. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldZeroWords.selected_window line 79
  11. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldZeroWords.complementary_window line 119
  12. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldZeroFinish.canonicalZero line 142
  13. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldZeroFinish.canonicalSelected line 143
  14. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldZeroFinish.physicalZero line 146
  15. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldZeroFinish.physicalSelected line 147
  16. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldZeroFinish.shape_has_zero line 149
  17. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldZeroFinish.canonicalZero_spec line 154
  18. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldZeroFinish.canonicalSelected_spec line 157
  19. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldZeroFinish.shape_total line 163
  20. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldZeroFinish.shape_total_pos line 166
  21. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldZeroFinish.axes_distinct line 170
  22. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldZeroFinish.physical_axes_distinct line 174
  23. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldZeroFinish.physical_shape line 177
  24. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldZeroFinish.nativeLaw line 183
  25. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldZeroFinish.selected_law line 187
  26. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldZeroFinish.zero_law line 200
  27. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldZeroFinish.remaining_law line 225
  28. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldZeroFinish.embed line 244
  29. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldZeroFinish.embed_window line 249
  30. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldZeroFinish.embed_mask line 281
  31. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldZeroFinish.coefficient line 296
  32. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldZeroFinish.Row line 309
  33. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldZeroFinish.Middle line 311
  34. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldZeroFinish.Column line 313
  35. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldZeroFinish.localMap line 316
  36. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldZeroFinish.volume line 325
  37. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldZeroFinish.dimensions_pos line 330