OAI/LinearAlgebra/MatrixMultiplication/FieldHistory/RecoveryCore.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Finite extraction histories, inherited masks and recovery bounds.

  1. theorem OAI.MatrixMultiplication.AllFieldHistoryRecovery.halfLength_le_eight line 24
  2. abbrev OAI.MatrixMultiplication.AllFieldHistoryRecovery.Raw line 28
  3. abbrev OAI.MatrixMultiplication.AllFieldHistoryRecovery.Targets line 31
  4. abbrev OAI.MatrixMultiplication.AllFieldHistoryRecovery.Symmetries line 34
  5. def OAI.MatrixMultiplication.AllFieldHistoryRecovery.childStatistic line 38
  6. def OAI.MatrixMultiplication.AllFieldHistoryRecovery.leftPrescription line 41
  7. def OAI.MatrixMultiplication.AllFieldHistoryRecovery.rightPrescription line 44
  8. def OAI.MatrixMultiplication.AllFieldHistoryRecovery.outputWidth line 47
  9. def OAI.MatrixMultiplication.AllFieldHistoryRecovery.parents line 50
  10. def OAI.MatrixMultiplication.AllFieldHistoryRecovery.rawSource line 54
  11. def OAI.MatrixMultiplication.AllFieldHistoryRecovery.ideal line 60
  12. def OAI.MatrixMultiplication.AllFieldHistoryRecovery.coordinates line 69
  13. def OAI.MatrixMultiplication.AllFieldHistoryRecovery.canonical line 74
  14. def OAI.MatrixMultiplication.AllFieldHistoryRecovery.rawAction line 84
  15. def OAI.MatrixMultiplication.AllFieldHistoryRecovery.completeKeep line 89
  16. def OAI.MatrixMultiplication.AllFieldHistoryRecovery.sideVariable line 96
  17. def OAI.MatrixMultiplication.AllFieldHistoryRecovery.idealSide line 98