OAI/LinearAlgebra/MatrixMultiplication/FieldHistory/GroupedRecovery.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Finite extraction histories, inherited masks and recovery bounds.

  1. theorem OAI.MatrixMultiplication.AllFieldHistoryGroupedRecovery.coordinates_project line 22
  2. theorem OAI.MatrixMultiplication.AllFieldHistoryGroupedRecovery.idealSide_iff_all_groups line 33
  3. theorem OAI.MatrixMultiplication.AllFieldHistoryGroupedRecovery.project_joinGroupTargets line 47
  4. def OAI.MatrixMultiplication.AllFieldHistoryGroupedRecovery.groupedAssignment line 57
  5. theorem OAI.MatrixMultiplication.AllFieldHistoryGroupedRecovery.groupedAssignment_sound line 71
  6. def OAI.MatrixMultiplication.AllFieldHistoryGroupedRecovery.localOrbit line 109
  7. def OAI.MatrixMultiplication.AllFieldHistoryGroupedRecovery.localAssigned line 116
  8. theorem OAI.MatrixMultiplication.AllFieldHistoryGroupedRecovery.grouped_assigned_iff line 123
  9. theorem OAI.MatrixMultiplication.AllFieldHistoryGroupedRecovery.filter_eq_rejected line 138
  10. theorem OAI.MatrixMultiplication.AllFieldHistoryGroupedRecovery.grouped_collision_le line 144
  11. theorem OAI.MatrixMultiplication.AllFieldHistoryGroupedRecovery.repair_grouped line 236