OAI/LinearAlgebra/MatrixMultiplication/FieldHistory/Produced.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Finite extraction histories, inherited masks and recovery bounds.

  1. def OAI.MatrixMultiplication.AllFieldHistoryProduced.passes line 21
  2. theorem OAI.MatrixMultiplication.AllFieldHistoryProduced.producedTensor_eq_delete line 25
  3. theorem OAI.MatrixMultiplication.AllFieldHistoryProduced.canonical_eq_delete line 34
  4. def OAI.MatrixMultiplication.AllFieldHistoryProduced.pulled line 58
  5. theorem OAI.MatrixMultiplication.AllFieldHistoryProduced.delete_pulled line 66
  6. def OAI.MatrixMultiplication.AllFieldHistoryProduced.pullbackMap line 85
  7. def OAI.MatrixMultiplication.AllFieldHistoryProduced.map line 94