OAI/Analysis/Kaplansky/Regular/ReducedTrace.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KaplanskyConsequences.Regular.delta line 16
  2. lemma OAI.KaplanskyConsequences.Regular.delta_apply line 17
  3. lemma OAI.KaplanskyConsequences.Regular.inner_delta line 19
  4. lemma OAI.KaplanskyConsequences.Regular.inner_delta_right line 22
  5. def OAI.KaplanskyConsequences.Regular.right line 27
  6. lemma OAI.KaplanskyConsequences.Regular.right_apply line 29
  7. lemma OAI.KaplanskyConsequences.Regular.right_star line 31
  8. lemma OAI.KaplanskyConsequences.Regular.left_commute_right line 39
  9. lemma OAI.KaplanskyConsequences.Regular.algebra_commute_right line 43
  10. lemma OAI.KaplanskyConsequences.Regular.right_delta line 55
  11. lemma OAI.KaplanskyConsequences.Regular.algebra_delta line 60
  12. lemma OAI.KaplanskyConsequences.Regular.algebra_star_delta line 68
  13. def OAI.KaplanskyConsequences.Regular.coefficient line 74
  14. lemma OAI.KaplanskyConsequences.Regular.coefficient_square line 75
  15. lemma OAI.KaplanskyConsequences.Regular.coefficient_tracial line 82
  16. lemma OAI.KaplanskyConsequences.Regular.delta_cyclic line 94
  17. lemma OAI.KaplanskyConsequences.Regular.coefficient_faithful line 111
  18. def OAI.KaplanskyConsequences.Regular.canonicalTrace line 115