OAI/Analysis/Pureness/Stabilization/MatrixMasks.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CuntzTrace.matrixMask line 11
  2. lemma OAI.CuntzTrace.matrixMask_apply line 14
  3. lemma OAI.CuntzTrace.matrixMask_eq_self line 17
  4. lemma OAI.CuntzTrace.matrixMask_zero line 21
  5. lemma OAI.CuntzTrace.matrixMask_add line 23
  6. lemma OAI.CuntzTrace.matrixMask_smul line 26
  7. lemma OAI.CuntzTrace.matrixMask_sub line 29
  8. def OAI.CuntzTrace.matrixUnitize line 33
  9. lemma OAI.CuntzTrace.matrixUnitize_injective line 36
  10. lemma OAI.CuntzTrace.matrixUnitize_norm line 41
  11. def OAI.CuntzTrace.matrixMaskProjection line 45
  12. lemma OAI.CuntzTrace.matrixMaskProjection_star line 48
  13. lemma OAI.CuntzTrace.matrixMaskProjection_mul line 54
  14. lemma OAI.CuntzTrace.matrixMaskProjection_norm_le line 66
  15. lemma OAI.CuntzTrace.matrixMask_unitize line 71
  16. theorem OAI.CuntzTrace.matrixMask_norm_le line 81
  17. lemma OAI.CuntzTrace.matrixMask_successor line 93
  18. lemma OAI.CuntzTrace.matrixMask_inclusion line 100