English
The multiples of a on AddCircle(p) form a dense range if and only if a/p is irrational.
Русский
Умножения на a в AddCircle(p) образуют плотный диапазон тогда, когда a/p иррационально.
LaTeX
$$$$ \\text{DenseRange}(\\,\\cdot \\; \\text{on } a) \\iff \\operatorname{Irrational}\\left(\\frac{a}{p}\\right). $$$$
Lean4
/-- The multiples of a number `a` are dense on a circle of length `p` iff `a / p` is irrational. -/
theorem denseRange_zsmul_coe_iff {a p : ℝ} : DenseRange (· • a : ℤ → AddCircle p) ↔ Irrational (a / p) := by
rw [← dense_addSubgroupClosure_pair_iff, DenseRange, ← QuotientAddGroup.dense_preimage_mk, ← QuotientAddGroup.coe_mk',
← AddSubgroup.coe_zmultiples, ← AddSubgroup.coe_comap, ← AddMonoidHom.map_zmultiples, AddSubgroup.comap_map_eq,
QuotientAddGroup.ker_mk', AddSubgroup.zmultiples_eq_closure, AddSubgroup.zmultiples_eq_closure, ←
AddSubgroup.closure_union, insert_eq]
