OAI/LinearAlgebra/MatrixMultiplication/FieldHistory/Regrouping.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Finite extraction histories, inherited masks and recovery bounds.

  1. abbrev OAI.MatrixMultiplication.AllFieldHistoryRegrouping.StateWords line 17
  2. abbrev OAI.MatrixMultiplication.AllFieldHistoryRegrouping.DueWords line 18
  3. abbrev OAI.MatrixMultiplication.AllFieldHistoryRegrouping.CarriedWords line 19
  4. abbrev OAI.MatrixMultiplication.AllFieldHistoryRegrouping.ActiveWords line 20
  5. abbrev OAI.MatrixMultiplication.AllFieldHistoryRegrouping.ProducedWords line 22
  6. instance OAI.MatrixMultiplication.AllFieldHistoryRegrouping.dueWordsFintype line 24
  7. instance OAI.MatrixMultiplication.AllFieldHistoryRegrouping.carriedWordsFintype line 27
  8. instance OAI.MatrixMultiplication.AllFieldHistoryRegrouping.activeWordsFintype line 30
  9. instance OAI.MatrixMultiplication.AllFieldHistoryRegrouping.producedWordsFintype line 34
  10. def OAI.MatrixMultiplication.AllFieldHistoryRegrouping.carriedTensor line 37
  11. def OAI.MatrixMultiplication.AllFieldHistoryRegrouping.activeTensor line 43
  12. def OAI.MatrixMultiplication.AllFieldHistoryRegrouping.producedTensor line 49
  13. def OAI.MatrixMultiplication.AllFieldHistoryRegrouping.toState line 55
  14. theorem OAI.MatrixMultiplication.AllFieldHistoryRegrouping.toState_due line 59
  15. theorem OAI.MatrixMultiplication.AllFieldHistoryRegrouping.toState_carried line 64
  16. def OAI.MatrixMultiplication.AllFieldHistoryRegrouping.dueTensorAt line 69
  17. theorem OAI.MatrixMultiplication.AllFieldHistoryRegrouping.split_coefficient line 75
  18. def OAI.MatrixMultiplication.AllFieldHistoryRegrouping.splitMap line 86
  19. def OAI.MatrixMultiplication.AllFieldHistoryRegrouping.toDue line 98
  20. theorem OAI.MatrixMultiplication.AllFieldHistoryRegrouping.active_coefficient line 103
  21. def OAI.MatrixMultiplication.AllFieldHistoryRegrouping.activeMap line 114
  22. def OAI.MatrixMultiplication.AllFieldHistoryRegrouping.activeCarriedMap line 125
  23. def OAI.MatrixMultiplication.AllFieldHistoryRegrouping.fromNext line 133
  24. theorem OAI.MatrixMultiplication.AllFieldHistoryRegrouping.next_coefficient line 138
  25. def OAI.MatrixMultiplication.AllFieldHistoryRegrouping.nextMap line 150