Irrational rotation is minimal

In this file we prove that the multiples of an irrational element of an AddCircle are dense. Moreover, an additive subgroup of the circle is dense iff it is not generated by a single element of finite additive order.

theorem dense_addSubgroupClosure_pair_iff {a b : ℝ} : Dense ↑(AddSubgroup.closure {a, b}) ↔ Irrational (a / b)

The additive subgroup of real numbers generated by a and b is dense iff a / b is an irrational number.

Here we rely on the fact that a / 0 = 0 in Mathlib, so we don't need to add b ≠ 0 as an assumption.

theorem AddCircle.denseRange_zsmul_coe_iff {a p : ℝ} : (DenseRange fun (x : ℤ) => x • ↑a) ↔ Irrational (a / p)

The multiples of a number a are dense on a circle of length p iff a / p is irrational.

theorem AddCircle.denseRange_zsmul_iff {p : ℝ} [Fact (0 < p)] {a : AddCircle p} : (DenseRange fun (x : ℤ) => x • a) ↔ addOrderOf a = 0

The multiples of a number a are dense on a circle of length p > 0 iff a has infinite additive order.

theorem AddCircle.dense_addSubgroup_iff_ne_zmultiples {p : ℝ} [Fact (0 < p)] {s : AddSubgroup (AddCircle p)} : Dense ↑s ↔ ∀ (a : AddCircle p), addOrderOf a ≠ 0 → s ≠ AddSubgroup.zmultiples a

A subgroup of the circle ℝ⧸pℤ, p > 0, is dense iff it is not generated by a single element of finite additive order.