OAI/Analysis/Commutator/CompletionCentered.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.HilbertCompletion.completeEquiv line 27
2. lemma OAI.Kadison.HilbertCompletion.completeEquiv_apply line 34
3. abbrev OAI.Kadison.HilbertCompletion.centered line 37
4. def OAI.Kadison.HilbertCompletion.centeredMap line 39
5. lemma OAI.Kadison.HilbertCompletion.centeredMap_coe line 52
6. lemma OAI.Kadison.HilbertCompletion.centeredMap_surjective line 56
7. def OAI.Kadison.HilbertCompletion.centeredEquiv line 84