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: Jan 04 2025 at 20:18 UTC