OAI/LinearAlgebra/MatrixMultiplication/FieldHistory/GroupAssignment.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Finite extraction histories, inherited masks and recovery bounds.

  1. def OAI.MatrixMultiplication.AllFieldHistory.activeEquivOrders line 18
  2. def OAI.MatrixMultiplication.AllFieldHistory.activeWordsEquivOrders line 22
  3. theorem OAI.MatrixMultiplication.AllFieldHistory.prod_active_eq_prod_orders line 33
  4. theorem OAI.MatrixMultiplication.AllFieldHistory.familyProduct_active_eq_orders line 41
  5. def OAI.MatrixMultiplication.AllFieldHistory.GroupAssignment.side line 57
  6. def OAI.MatrixMultiplication.AllFieldHistory.GroupAssignment.restorePhysical line 60
  7. theorem OAI.MatrixMultiplication.AllFieldHistory.GroupAssignment.side_restorePhysical line 66
  8. def OAI.MatrixMultiplication.AllFieldHistory.GroupAssignment.collect line 73
  9. theorem OAI.MatrixMultiplication.AllFieldHistory.GroupAssignment.collect_eq_some line 77
  10. theorem OAI.MatrixMultiplication.AllFieldHistory.GroupAssignment.collect_failure_iff line 95
  11. def OAI.MatrixMultiplication.AllFieldHistory.GroupAssignment.product line 102
  12. theorem OAI.MatrixMultiplication.AllFieldHistory.GroupAssignment.product_coherent line 110
  13. theorem OAI.MatrixMultiplication.AllFieldHistory.GroupAssignment.product_branch line 129
  14. def OAI.MatrixMultiplication.AllFieldHistory.groupedSideAssignment line 159
  15. theorem OAI.MatrixMultiplication.AllFieldHistory.groupedSideAssignment_eq_some line 164
  16. def OAI.MatrixMultiplication.AllFieldHistory.groupedAssignment line 171
  17. theorem OAI.MatrixMultiplication.AllFieldHistory.groupedAssignment_coherent line 181
  18. theorem OAI.MatrixMultiplication.AllFieldHistory.groupedAssignment_branch line 199
  19. def OAI.MatrixMultiplication.AllFieldHistory.joinGroupTargets line 226
  20. theorem OAI.MatrixMultiplication.AllFieldHistory.joinGroupTargets_apply line 232
  21. theorem OAI.MatrixMultiplication.AllFieldHistory.joinGroupTargets_on_group line 238
  22. theorem OAI.MatrixMultiplication.AllFieldHistory.joinGroupTargets_injective line 248