OAI/Analysis/Commutator/DihedralCompressionMoments.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Kadison.DihedralCorner.corner_wave_pairing line 35
2. theorem OAI.Kadison.DihedralCorner.free_compression_wave_pairing line 46
3. lemma OAI.Kadison.DihedralCorner.reflection_corner line 64
4. lemma OAI.Kadison.DihedralCorner.rotation_sandwich_trace line 71
5. lemma OAI.Kadison.DihedralCorner.symmetry_wave_product line 79
6. lemma OAI.Kadison.DihedralCorner.symmetry_sandwich_trace line 87
7. lemma OAI.Kadison.DihedralCorner.wave_corner_even line 105
8. lemma OAI.Kadison.DihedralCorner.compression_rotation_sandwich line 113
9. lemma OAI.Kadison.DihedralCorner.compression_symmetry_sandwich line 124