OAI/LinearAlgebra/MatrixMultiplication/FieldHistory/Source.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Finite extraction histories, inherited masks and recovery bounds.

  1. def OAI.MatrixMultiplication.AllFieldHistorySource.deleteWithPred line 19
  2. abbrev OAI.MatrixMultiplication.AllFieldHistorySource.Raw line 32
  3. def OAI.MatrixMultiplication.AllFieldHistorySource.toActive line 34
  4. theorem OAI.MatrixMultiplication.AllFieldHistorySource.parent_coefficient line 37
  5. def OAI.MatrixMultiplication.AllFieldHistorySource.receivedSource line 65
  6. theorem OAI.MatrixMultiplication.AllFieldHistorySource.received_coefficient line 70
  7. def OAI.MatrixMultiplication.AllFieldHistorySource.receivedMap line 101
  8. def OAI.MatrixMultiplication.AllFieldHistorySource.marginal line 112
  9. def OAI.MatrixMultiplication.AllFieldHistorySource.preparedSource line 116
  10. theorem OAI.MatrixMultiplication.AllFieldHistorySource.preparedSource_eq_delete line 123
  11. def OAI.MatrixMultiplication.AllFieldHistorySource.preparedMap line 135
  12. abbrev OAI.MatrixMultiplication.AllFieldHistorySource.GroupWords line 143
  13. def OAI.MatrixMultiplication.AllFieldHistorySource.groupsEquiv line 146
  14. theorem OAI.MatrixMultiplication.AllFieldHistorySource.project_groups_symm line 152
  15. theorem OAI.MatrixMultiplication.AllFieldHistorySource.grouped_coefficient line 158
  16. def OAI.MatrixMultiplication.AllFieldHistorySource.groupsMap line 169