OAI/Analysis/CharacterCriterion/FourLegSymmetries.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.KirchbergRordam.FourLegSymmetries.Index line 37
2. abbrev OAI.KirchbergRordam.FourLegSymmetries.Algebra line 38
3. def OAI.KirchbergRordam.FourLegSymmetries.hflip line 39
4. def OAI.KirchbergRordam.FourLegSymmetries.kflip line 44
5. def OAI.KirchbergRordam.FourLegSymmetries.H line 49
6. def OAI.KirchbergRordam.FourLegSymmetries.K line 50
7. lemma OAI.KirchbergRordam.FourLegSymmetries.H_selfadjoint line 51
8. lemma OAI.KirchbergRordam.FourLegSymmetries.K_selfadjoint line 55
9. lemma OAI.KirchbergRordam.FourLegSymmetries.flips_commute line 59
10. lemma OAI.KirchbergRordam.FourLegSymmetries.flip_product line 63
11. lemma OAI.KirchbergRordam.FourLegSymmetries.conj_flip_left line 66
12. lemma OAI.KirchbergRordam.FourLegSymmetries.conj_K_left_left line 74
13. lemma OAI.KirchbergRordam.FourLegSymmetries.conj_H_right_right line 88
14. lemma OAI.KirchbergRordam.FourLegSymmetries.H_decompose line 106
15. lemma OAI.KirchbergRordam.FourLegSymmetries.K_decompose line 120
16. lemma OAI.KirchbergRordam.FourLegSymmetries.H_mem line 134
17. lemma OAI.KirchbergRordam.FourLegSymmetries.K_mem line 140
18. lemma OAI.KirchbergRordam.FourLegSymmetries.conj_K_left_right line 146
19. lemma OAI.KirchbergRordam.FourLegSymmetries.conj_H_left_left line 158
20. lemma OAI.KirchbergRordam.FourLegSymmetries.conj_H_left_right line 170
21. lemma OAI.KirchbergRordam.FourLegSymmetries.K_cross_mem line 183
22. lemma OAI.KirchbergRordam.FourLegSymmetries.H_cross_mem line 194