Email Gateway (Sep 21 2023 at 13:47): Email Gateway (Sep 21 2023 at 13:47):From: Stepan Holub <holub@karlin.mff.cuni.cz>
Dear all,
are you aware of an Isabelle development connected to real numbers
modulo one?
Think for example of the claim that the additive subgroup generated by
an irrational number is dense.
Best regards
Stepan
Last updated: Apr 28 2024 at 20:16 UTC