OAI/Analysis/Pureness/Stabilization/MatrixTripleLayout.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CuntzTrace.le_double line 10
  2. def OAI.CuntzTrace.matrixTripleLeftIndex line 12
  3. def OAI.CuntzTrace.matrixTripleRightIndex line 17
  4. lemma OAI.CuntzTrace.matrixTripleLeftIndex_injective line 22
  5. lemma OAI.CuntzTrace.matrixTripleRightIndex_injective line 29
  6. def OAI.CuntzTrace.matrixTripleLeft line 36
  7. def OAI.CuntzTrace.matrixTripleRight line 39
  8. lemma OAI.CuntzTrace.matrixTriple_entries line 42
  9. lemma OAI.CuntzTrace.matrixTripleLeft_outside line 51
  10. lemma OAI.CuntzTrace.matrixTripleRight_outside line 72
  11. theorem OAI.CuntzTrace.matrixTriple_permutation line 93