Theorems · Theorem · general topology

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.

Defined in

Mathlib.Topology.Instances.AddCircle.DenseSubgroup

Cited by

1 results in Mathlib

Foundations

Depth 119 from the axioms · uses propext, Classical.choice, Quot.sound