OAI/Analysis/IrrationalRotation/Rotation/ContinuousCircleImage.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.ContinuousCircleImage.fourier_natCast line 14
2. theorem OAI.Invariant233.ContinuousCircleImage.isClosed_vonNeumannAlgebra line 27
3. theorem OAI.Invariant233.ContinuousCircleImage.image_mem line 32
4. theorem OAI.Invariant233.ContinuousCircleImage.hom_ext_character line 64