OAI/Analysis/IrrationalRotation/Operators/Commutant.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.Commutant.mem_iff line 9
2. theorem OAI.Invariant233.Commutant.one_mem line 14
3. theorem OAI.Invariant233.Commutant.isClosed_strong_commutant line 18
4. theorem OAI.Invariant233.Commutant.commute_of_strong_limit line 27
5. theorem OAI.Invariant233.operatorCommutant_mem_iff line 45
6. theorem OAI.Invariant233.operatorCommutant_stronglyClosed line 49
7. theorem OAI.Invariant233.operatorCommutant_transitive_iff line 61
8. theorem OAI.Invariant233.IsHyperinvariant.isInvariant line 69