mathlib3

72944168 - feat(topology/instances/real): classify discrete subgroups (#16592)

feat(topology/instances/real): classify discrete subgroups (#16592) The subgroups aℤ (i.e. `zmultiples a`) of ℝ are discrete, in the sense of having finite intersection with any compact subset. Co-authored-by: Alex Kontorovich <58564076+AlexKontorovich@users.noreply.github.com>