OAI/Analysis/Pureness/Stabilization/MatrixParityClasses.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CuntzTrace.matrixParityEmbedding line 11
  2. def OAI.CuntzTrace.matrixParity line 15
  3. lemma OAI.CuntzTrace.matrixParity_embedding line 19
  4. lemma OAI.CuntzTrace.matrixParity_stage line 37
  5. theorem OAI.CuntzTrace.matrixLimit_maps_eq line 43
  6. theorem OAI.CuntzTrace.matrixParity_cuntzClass line 60
  7. instance OAI.CuntzTrace.CuntzClass.(instance at line 71) line 71
  8. lemma OAI.CuntzTrace.CuntzClass.zero_mk line 72
  9. theorem OAI.CuntzTrace.CuntzClass.matrixAdd_zero line 74
  10. theorem OAI.CuntzTrace.CuntzClass.zero_matrixAdd line 83