OAI/Analysis/Pureness/Stabilization/RankCyclic.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CuntzTrace.supported_cfc_factor line 12
  2. lemma OAI.CuntzTrace.ExtendedTrace.tracial_supported_cfc line 32
  3. lemma OAI.CuntzTrace.ExtendedTrace.tracial_power_cut line 68
  4. lemma OAI.CuntzTrace.ExtendedTrace.tracial_power_le line 89
  5. theorem OAI.CuntzTrace.ExtendedTrace.tracial_power line 104
  6. theorem OAI.CuntzTrace.ExtendedTrace.rank_tracial line 110
  7. def OAI.CuntzTrace.Positive.conjugate line 120
  8. lemma OAI.CuntzTrace.Positive.conjugate_eq_starMul line 123
  9. lemma OAI.CuntzTrace.Positive.mulStar_sqrt_mul_le line 132
  10. lemma OAI.CuntzTrace.ExtendedTrace.rank_conjugate_le line 148
  11. theorem OAI.CuntzTrace.ExtendedTrace.rank_le_of_cuntzBelow line 154
  12. theorem OAI.CuntzTrace.ExtendedTrace.rank_eq_of_cuntzEquivalent line 171