OAI/Analysis/Commutator/TensorActions.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.completionIsometry line 20
2. lemma OAI.Kadison.completionIsometry_coe line 27
3. def OAI.Kadison.PreHilbert.powerMap line 36
4. lemma OAI.Kadison.PreHilbert.powerMap_pure line 40
5. def OAI.Kadison.PreHilbert.wordMap line 49
6. lemma OAI.Kadison.PreHilbert.wordMap_word line 53
7. lemma OAI.Kadison.coefficient_invariant line 67