OAI/Analysis/Commutator/HilbertTensors.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.Kadison.PreHilbert line 13
2. instance OAI.Kadison.(instance at line 20) line 20
3. abbrev OAI.Kadison.PreHilbert.scalar line 24
4. abbrev OAI.Kadison.PreHilbert.tensor line 26
5. def OAI.Kadison.PreHilbert.power line 28
6. def OAI.Kadison.PreHilbert.pure line 32
7. theorem OAI.Kadison.PreHilbert.pure_zero line 36
8. theorem OAI.Kadison.PreHilbert.pure_succ line 39
9. theorem OAI.Kadison.PreHilbert.norm_pure line 42
10. theorem OAI.Kadison.PreHilbert.inner_pure line 50
11. theorem OAI.Kadison.PreHilbert.span_pure line 58