OAI/LinearAlgebra/MatrixMultiplication/FieldHistory/Tick.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Finite extraction histories, inherited masks and recovery bounds.

  1. abbrev OAI.MatrixMultiplication.AllFieldHistoryTick.Choices line 23
  2. abbrev OAI.MatrixMultiplication.AllFieldHistoryTick.AmbientTag line 26
  3. abbrev OAI.MatrixMultiplication.AllFieldHistoryTick.Tags line 30
  4. def OAI.MatrixMultiplication.AllFieldHistoryTick.coarseTripleFintype line 37
  5. instance OAI.MatrixMultiplication.AllFieldHistoryTick.ambientTagFintype line 40
  6. instance OAI.MatrixMultiplication.AllFieldHistoryTick.ambientTagsFintype line 44
  7. instance OAI.MatrixMultiplication.AllFieldHistoryTick.tagsFintype line 47
  8. def OAI.MatrixMultiplication.AllFieldHistoryTick.select line 50
  9. theorem OAI.MatrixMultiplication.AllFieldHistoryTick.select_injective line 55
  10. def OAI.MatrixMultiplication.AllFieldHistoryTick.targets line 63
  11. def OAI.MatrixMultiplication.AllFieldHistoryTick.assignments line 68
  12. def OAI.MatrixMultiplication.AllFieldHistoryTick.assignment line 77
  13. theorem OAI.MatrixMultiplication.AllFieldHistoryTick.coherent line 81
  14. theorem OAI.MatrixMultiplication.AllFieldHistoryTick.repair line 91
  15. def OAI.MatrixMultiplication.AllFieldHistoryTick.canonicalMap line 130
  16. def OAI.MatrixMultiplication.AllFieldHistoryTick.activeExecution line 144
  17. theorem OAI.MatrixMultiplication.AllFieldHistoryTick.activeExecution_copies line 165
  18. theorem OAI.MatrixMultiplication.AllFieldHistoryTick.card_tags line 175
  19. def OAI.MatrixMultiplication.AllFieldHistoryTick.execution line 184
  20. theorem OAI.MatrixMultiplication.AllFieldHistoryTick.execution_copies line 193