OAI/Analysis/Commutator/StandardTrace.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Kadison.NormalGNS.gns_injective line 24
  2. lemma OAI.Kadison.NormalGNS.gns_norm line 36
  3. def OAI.Kadison.NormalGNS.algebra line 42
  4. lemma OAI.Kadison.NormalGNS.mem_algebra line 45
  5. def OAI.Kadison.NormalGNS.equivalence line 48
  6. lemma OAI.Kadison.NormalGNS.equivalence_apply line 52
  7. def OAI.Kadison.NormalGNS.trace line 55
  8. lemma OAI.Kadison.NormalGNS.trace_gns line 57
  9. lemma OAI.Kadison.NormalGNS.trace_continuous line 62
  10. lemma OAI.Kadison.NormalGNS.trace_tracial line 66
  11. lemma OAI.Kadison.NormalGNS.trace_faithful line 82
  12. lemma OAI.Kadison.NormalGNS.trace_one line 91
  13. theorem OAI.Kadison.NormalGNS.isFactor line 95