OAI/Analysis/Kaplansky/Quotient/Extraction.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.KaplanskyConsequences.no_tracialState_of_finite_obstruction line 15
  2. theorem OAI.KaplanskyConsequences.stablyFinite_of_injective line 35
  3. theorem OAI.KaplanskyConsequences.finite_generated_extraction line 51
  4. def OAI.KaplanskyConsequences.selfCommutator line 72
  5. def OAI.KaplanskyConsequences.commutatorSpan line 75
  6. def OAI.KaplanskyConsequences.positiveCone line 78
  7. lemma OAI.KaplanskyConsequences.positiveCone_convex line 81
  8. lemma OAI.KaplanskyConsequences.one_mem_interior_positiveCone line 86
  9. lemma OAI.KaplanskyConsequences.trace_identity_of_square_swap line 100
  10. def OAI.KaplanskyConsequences.complexify line 116
  11. lemma OAI.KaplanskyConsequences.complexify_apply_selfAdjoint line 119
  12. lemma OAI.KaplanskyConsequences.tracialState_of_selfAdjoint_functional line 127
  13. lemma OAI.KaplanskyConsequences.nonpositive_functional_one_ne_zero line 150
  14. lemma OAI.KaplanskyConsequences.tracialState_of_disjoint line 170
  15. lemma OAI.KaplanskyConsequences.positive_commutator_of_no_trace line 206
  16. lemma OAI.KaplanskyConsequences.selfCommutator_star line 216
  17. lemma OAI.KaplanskyConsequences.selfCommutator_smul line 220
  18. lemma OAI.KaplanskyConsequences.smul_selfCommutator line 227
  19. lemma OAI.KaplanskyConsequences.commutatorSpan_finite_representation line 235
  20. lemma OAI.KaplanskyConsequences.strictly_positive_of_interior line 252
  21. lemma OAI.KaplanskyConsequences.strictly_positive_finite_selfCommutators line 267
  22. lemma OAI.KaplanskyConsequences.normalize_selfCommutators line 279
  23. theorem OAI.KaplanskyConsequences.finite_trace_obstruction line 337
  24. theorem OAI.KaplanskyConsequences.separable_extraction line 348