OAI/Analysis/IrrationalRotation/Operators/DenseOperatorRange.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.OperatorRange.denseRange_of_adjoint_injective line 14
2. theorem OAI.Invariant233.OperatorRange.denseRange_of_selfAdjoint_injective line 21
3. theorem OAI.Invariant233.OperatorRange.unitary_injective line 26
4. theorem OAI.Invariant233.OperatorRange.unitary_surjective line 33
5. theorem OAI.Invariant233.OperatorRange.unitary_mul_selfAdjoint_range line 40
6. theorem OAI.Invariant233.OperatorRange.not_surjective_of_zero_mem_spectrum line 49
7. theorem OAI.Invariant233.OperatorRange.not_isClosed_range_of_dense_not_surjective line 58
8. theorem OAI.Invariant233.OperatorRange.eq_zero_of_eigenvector_of_spectrum_zero line 69