OAI/LinearAlgebra/MatrixMultiplication/FieldHistory/Iteration.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Finite extraction histories, inherited masks and recovery bounds.

  1. def OAI.MatrixMultiplication.AllFieldHistoryIteration.retarget line 21
  2. theorem OAI.MatrixMultiplication.AllFieldHistoryIteration.retarget_copies line 32
  3. abbrev OAI.MatrixMultiplication.AllFieldHistoryIteration.ScheduleChoices line 39
  4. def OAI.MatrixMultiplication.AllFieldHistoryIteration.Labels line 42
  5. instance OAI.MatrixMultiplication.AllFieldHistoryIteration.labelsFintype line 50
  6. theorem OAI.MatrixMultiplication.AllFieldHistoryIteration.card_labels line 61
  7. abbrev OAI.MatrixMultiplication.AllFieldHistoryIteration.Tags line 79
  8. theorem OAI.MatrixMultiplication.AllFieldHistoryIteration.card_tags line 83
  9. def OAI.MatrixMultiplication.AllFieldHistoryIteration.run line 99
  10. theorem OAI.MatrixMultiplication.AllFieldHistoryIteration.run_copies line 116
  11. def OAI.MatrixMultiplication.AllFieldHistoryIteration.execution line 131
  12. theorem OAI.MatrixMultiplication.AllFieldHistoryIteration.execution_copies line 137