OAI/Analysis/Commutator/TensorPermutations3.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.PreHilbert.permute line 69
2. theorem OAI.Kadison.PreHilbert.permute_pure line 86
3. def OAI.Kadison.PreHilbert.hilbertPermute line 90
4. theorem OAI.Kadison.PreHilbert.hilbertPermute_pure line 98
5. theorem OAI.Kadison.PreHilbert.eq_zero_of_hilbertPure_inner line 108
6. theorem OAI.Kadison.PreHilbert.continuousLinearMap_ext_pure line 119