OAI/LinearAlgebra/MatrixMultiplication/FieldHistory/Geometry.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Finite extraction histories, inherited masks and recovery bounds.

  1. def OAI.MatrixMultiplication.AllFieldHistory.currentShape line 13
  2. def OAI.MatrixMultiplication.AllFieldHistory.currentLength line 20
  3. def OAI.MatrixMultiplication.AllFieldHistory.currentPhysicalShape line 26
  4. theorem OAI.MatrixMultiplication.AllFieldHistory.currentShape_spec line 29
  5. theorem OAI.MatrixMultiplication.AllFieldHistory.currentPhysicalShape_total line 48
  6. theorem OAI.MatrixMultiplication.AllFieldHistory.positive_iff_no_zero line 52
  7. theorem OAI.MatrixMultiplication.AllFieldHistory.not_positive_has_zero line 69
  8. theorem OAI.MatrixMultiplication.AllFieldHistory.terminal_has_zero line 76
  9. theorem OAI.MatrixMultiplication.AllFieldHistory.terminal_physical_zero line 91
  10. theorem OAI.MatrixMultiplication.AllFieldHistory.final_physical_zero line 96
  11. theorem OAI.MatrixMultiplication.AllFieldHistory.source_shape line 100
  12. theorem OAI.MatrixMultiplication.AllFieldHistory.source_length line 103
  13. theorem OAI.MatrixMultiplication.AllFieldHistory.child_shape line 106
  14. theorem OAI.MatrixMultiplication.AllFieldHistory.child_length line 110