OAI/Analysis/Commutator/PartialUnitaryHom.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.FinitePatching.PartialUnitary.map line 22
2. lemma OAI.Kadison.FinitePatching.PartialUnitary.map_power line 32
3. lemma OAI.Kadison.FinitePatching.PartialUnitary.map_ofUnitary line 39
4. lemma OAI.Kadison.FinitePatching.PartialUnitary.ofUnitary_power_one line 45
5. lemma OAI.Kadison.FinitePatching.PartialUnitary.ofUnitary_power_neg_one line 49
6. lemma OAI.Kadison.FinitePatching.Words.map_slotPower line 58
7. lemma OAI.Kadison.FinitePatching.Words.map_letter line 68
8. lemma OAI.Kadison.FinitePatching.Words.map_word line 73
9. lemma OAI.Kadison.FinitePatching.PartialUnitary.map_power_algebra line 89
10. lemma OAI.Kadison.FinitePatching.PartialUnitary.map_ofUnitary_algebra line 95
11. lemma OAI.Kadison.FinitePatching.Words.map_word_algebra line 106