OAI/LinearAlgebra/MatrixMultiplication/FieldHistory/Positions.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Finite extraction histories, inherited masks and recovery bounds.

  1. abbrev OAI.MatrixMultiplication.AllFieldHistory.ProducedPositions line 13
  2. abbrev OAI.MatrixMultiplication.AllFieldHistory.SplitPositions line 16
  3. def OAI.MatrixMultiplication.AllFieldHistory.halfPosition line 20
  4. def OAI.MatrixMultiplication.AllFieldHistory.unhalfPosition line 26
  5. theorem OAI.MatrixMultiplication.AllFieldHistory.unhalf_halfPosition line 32
  6. theorem OAI.MatrixMultiplication.AllFieldHistory.half_unhalfPosition line 37
  7. def OAI.MatrixMultiplication.AllFieldHistory.splitToProduced line 42
  8. def OAI.MatrixMultiplication.AllFieldHistory.producedToSplit line 61
  9. theorem OAI.MatrixMultiplication.AllFieldHistory.producedToSplit_splitToProduced line 82
  10. theorem OAI.MatrixMultiplication.AllFieldHistory.splitToProduced_producedToSplit line 107
  11. def OAI.MatrixMultiplication.AllFieldHistory.producedPositionEquiv line 132
  12. theorem OAI.MatrixMultiplication.AllFieldHistory.producedPositionEquiv_parent line 140
  13. theorem OAI.MatrixMultiplication.AllFieldHistory.producedPositionEquiv_shape line 151
  14. theorem OAI.MatrixMultiplication.AllFieldHistory.producedPositionEquiv_length line 167