OAI/Analysis/Pureness/Stabilization/MatrixBlock.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CuntzTrace.matrixPairLeft line 10
  2. def OAI.CuntzTrace.matrixPairRight line 18
  3. def OAI.CuntzTrace.matrixEvenStage line 26
  4. def OAI.CuntzTrace.matrixOddStage line 28
  5. lemma OAI.CuntzTrace.matrixEvenStage_compatible line 31
  6. lemma OAI.CuntzTrace.matrixOddStage_compatible line 34
  7. def OAI.CuntzTrace.matrixEven line 38
  8. def OAI.CuntzTrace.matrixOdd line 39
  9. lemma OAI.CuntzTrace.matrixEven_stage line 41
  10. lemma OAI.CuntzTrace.matrixOdd_stage line 43
  11. theorem OAI.CuntzTrace.matrixEven_mul_matrixOdd line 46
  12. theorem OAI.CuntzTrace.matrixOdd_mul_matrixEven line 70
  13. def OAI.CuntzTrace.matrixBlockHom line 74