OAI/Analysis/Commutator/HilbertBiprod.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Kadison.HilbertBiprod.Space line 18
  2. def OAI.Kadison.HilbertBiprod.inlL line 20
  3. def OAI.Kadison.HilbertBiprod.inrL line 24
  4. lemma OAI.Kadison.HilbertBiprod.inlL_apply line 28
  5. lemma OAI.Kadison.HilbertBiprod.inrL_apply line 30
  6. def OAI.Kadison.HilbertBiprod.inl line 32
  7. def OAI.Kadison.HilbertBiprod.inr line 37
  8. lemma OAI.Kadison.HilbertBiprod.inl_apply line 42
  9. lemma OAI.Kadison.HilbertBiprod.inr_apply line 44
  10. def OAI.Kadison.HilbertBiprod.block line 46
  11. lemma OAI.Kadison.HilbertBiprod.block_apply line 50
  12. lemma OAI.Kadison.HilbertBiprod.ext line 53
  13. lemma OAI.Kadison.HilbertBiprod.block_zero line 58
  14. lemma OAI.Kadison.HilbertBiprod.block_one line 63
  15. lemma OAI.Kadison.HilbertBiprod.block_mul line 68
  16. lemma OAI.Kadison.HilbertBiprod.block_add line 74
  17. lemma OAI.Kadison.HilbertBiprod.block_smul line 80
  18. lemma OAI.Kadison.HilbertBiprod.block_star line 88
  19. def OAI.Kadison.HilbertBiprod.diagHom line 99
  20. lemma OAI.Kadison.HilbertBiprod.diagHom_apply line 110
  21. lemma OAI.Kadison.HilbertBiprod.block_inl line 114
  22. lemma OAI.Kadison.HilbertBiprod.block_inr line 118
  23. lemma OAI.Kadison.HilbertBiprod.diagHom_injective line 121