English
The additive subgroup generated by two numbers a and b is dense in the circle if and only if a/b is irrational.
Русский
Аддитивная подгруппа, порождаемая двумя числами a и b, плотна в круге тогда и только тогда, когда отношение a/b иррационально.
LaTeX
$$$$ \\text{Dense}(\\mathrm{AddSubgroup}.closure\\{a,b\\}) \\iff \\operatorname{Irrational}\\left(\\frac{a}{b}\\right). $$$$
Lean4
/-- 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 dense_addSubgroupClosure_pair_iff {a b : ℝ} :
Dense (AddSubgroup.closure { a, b } : Set ℝ) ↔ Irrational (a / b) :=
by
rcases eq_or_ne b 0 with rfl | hb
· rw [pair_comm]
simpa [← AddSubgroup.zmultiples_eq_closure] using not_denseRange_zsmul
constructor
· rintro hd ⟨r, hr⟩
refine not_denseRange_zsmul (a := b / r.den) <| hd.mono ?_
rw [← AddSubgroup.coe_zmultiples, SetLike.coe_subset_coe, AddSubgroup.closure_le, AddSubgroup.coe_zmultiples,
pair_subset_iff]
refine ⟨⟨r.num, ?_⟩, r.den, ?_⟩
· simp [field, mul_div_left_comm _ b, ← Rat.cast_def, hr]
· simp [field]
· intro h
contrapose! h
rcases (AddSubgroup.dense_or_cyclic _).resolve_left h with ⟨c, hc⟩
have : { a, b } ⊆ range (· • c : ℤ → ℝ) :=
by
rw [← AddSubgroup.coe_zmultiples, AddSubgroup.zmultiples_eq_closure, ← hc]
apply AddSubgroup.subset_closure
rcases pair_subset_iff.1 this with ⟨⟨m, rfl⟩, n, rfl⟩
simp_all [mul_div_mul_right]
