OAI/Analysis/IrrationalRotation/Operators/TracialInverseClosure.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.inverse_mem_of_two_sided_inverse line 12
2. theorem OAI.Invariant233.IsFaithfulTracialVector.left_inverse_mem line 23
3. theorem OAI.Invariant233.IsFaithfulTracialVector.isUnit_of_ambient_left_inverse line 28
4. theorem OAI.Invariant233.IsFaithfulTracialVector.reverse_mul_eq_one line 36
5. theorem OAI.Invariant233.IsFaithfulTracialVector.right_inverse_mem line 44
6. theorem OAI.Invariant233.IsFaithfulTracialVector.isUnit_of_ambient_right_inverse line 49