OAI/Computability/PerfectCompleteness/Algebra/LowerCutNodeMatrix.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.LowerCutNodeMatrix.NativeMatrix line 17
  2. abbrev OAI.PerfectCompleteness.LowerCutNodeMatrix.NodeMatrix line 21
  3. def OAI.PerfectCompleteness.LowerCutNodeMatrix.matrixEquiv line 25
  4. theorem OAI.PerfectCompleteness.LowerCutNodeMatrix.ofRows_transport line 32
  5. theorem OAI.PerfectCompleteness.LowerCutNodeMatrix.rows_transport line 41
  6. theorem OAI.PerfectCompleteness.LowerCutNodeMatrix.selectedRows_matrix line 50
  7. theorem OAI.PerfectCompleteness.LowerCutNodeMatrix.shift_transport line 58
  8. theorem OAI.PerfectCompleteness.LowerCutNodeMatrix.replace_matrix_transport line 71
  9. theorem OAI.PerfectCompleteness.LowerCutNodeMatrix.uniform_matrixEquiv line 99
  10. theorem OAI.PerfectCompleteness.LowerCutNodeMatrix.uniform_matrix_scalarEquiv line 107
  11. theorem OAI.PerfectCompleteness.LowerCutNodeMatrix.uniform_stepPair_transport line 122