OAI/LinearAlgebra/MatrixFields/Construction/Subdivision.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatrixAllFields.MatrixMultiplication.Subdivision.concatenate line 23
  2. def OAI.MatrixAllFields.MatrixMultiplication.Subdivision.concatenateEquiv line 26
  3. theorem OAI.MatrixAllFields.MatrixMultiplication.Subdivision.wordPopulation_concatenate line 37
  4. theorem OAI.MatrixAllFields.MatrixMultiplication.Subdivision.empiricalLaw_concatenate line 48
  5. def OAI.MatrixAllFields.MatrixMultiplication.Subdivision.partWindows line 71
  6. theorem OAI.MatrixAllFields.MatrixMultiplication.Subdivision.typeWindow_concatenate line 75
  7. theorem OAI.MatrixAllFields.MatrixMultiplication.Subdivision.statisticWindow_concatenate line 103
  8. def OAI.MatrixAllFields.MatrixMultiplication.Subdivision.positionsOfCounts line 114
  9. theorem OAI.MatrixAllFields.MatrixMultiplication.Subdivision.typeWindow_reindex line 118
  10. theorem OAI.MatrixAllFields.MatrixMultiplication.Subdivision.statisticWindow_concatenate_at line 126
  11. def OAI.MatrixAllFields.MatrixMultiplication.Subdivision.repeated line 143
  12. def OAI.MatrixAllFields.MatrixMultiplication.Subdivision.allParts line 146
  13. def OAI.MatrixAllFields.MatrixMultiplication.Subdivision.subdivisionMatrix line 149
  14. theorem OAI.MatrixAllFields.MatrixMultiplication.Subdivision.subdivisionMatrix_apply line 153
  15. theorem OAI.MatrixAllFields.MatrixMultiplication.Subdivision.restrict_received line 167
  16. def OAI.MatrixAllFields.MatrixMultiplication.Subdivision.subdivisionMatrixAt line 195
  17. theorem OAI.MatrixAllFields.MatrixMultiplication.Subdivision.restrict_received_at line 201