English
A subgroup of AddCircle(p) is dense iff it is not generated by a single element of finite additive order.
Русский
Подгруппа AddCircle(p) плотна тогда, когда она не порождается одним элементом конечного порядка сложения.
LaTeX
$$$$ \\text{Dense}(s) \\iff \\forall a, \\operatorname{addOrderOf}(a) \\neq 0 \\Rightarrow s \\neq \\mathrm{zmultiples}(a). $$$$
Lean4
/-- A subgroup of the circle `ℝ⧸pℤ`, `p > 0`, is dense
iff it is not generated by a single element of finite additive order. -/
theorem dense_addSubgroup_iff_ne_zmultiples {p : ℝ} [Fact (0 < p)] {s : AddSubgroup (AddCircle p)} :
Dense (s : Set (AddCircle p)) ↔ ∀ a, addOrderOf a ≠ 0 → s ≠ .zmultiples a :=
by
constructor
· rintro hd a ha rfl
rw [AddSubgroup.coe_zmultiples, ← DenseRange, denseRange_zsmul_iff] at hd
exact ha hd
· intro h
contrapose! h
obtain ⟨a, rfl⟩ : ∃ a, s = .zmultiples a :=
by
rw [← QuotientAddGroup.dense_preimage_mk, ← QuotientAddGroup.coe_mk', ← AddSubgroup.coe_comap,
xor_iff_not_iff'.1 (AddSubgroup.dense_xor'_cyclic _)] at h
rcases h with ⟨a, ha⟩
use a
rw [← QuotientAddGroup.coe_mk', ← AddMonoidHom.map_zmultiples, ← ha, AddSubgroup.map_comap_eq_self_of_surjective]
exact Quot.mk_surjective
exact ⟨a, denseRange_zsmul_iff.not.mp h, rfl⟩
