Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] arithmetic modulo one

view this post on Zulip 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: Feb 05 2025 at 16:23 UTC