p. 2 — a subring A ≠ ℤ of ℝ contains a countable dense subring

Proved

Monod.exists_countable_dense_subring_of_ne_bot

by dbenbenn · Sep 30, 2026 · Mathlib 0df444a (Lean v4.33.1)

amenabilitygroup-theorypiecewise-projective

If $A$ is a subring of $\mathbf{R}$ other than $\mathbf{Z}$ , there is a subring $A' \subseteq A$ that is countable and dense in $\mathbf{R}$ .

Preamble

import Mathlib

Formal statement

namespace Monod

theorem exists_countable_dense_subring_of_ne_bot {A : Subring ℝ} (hA : A ≠ ⊥) :
    ∃ A' : Subring ℝ, A' ≤ A ∧ Countable A' ∧ Dense (A' : Set ℝ) := by
  sorry

end Monod

Source

Monod, N., Groups of piecewise projective homeomorphisms, Proc. Natl. Acad. Sci. USA 110 (2013) 4524–4527, https://doi.org/10.1073/pnas.1218426110 (arXiv:1209.5229v2, whose page numbers are used), p. 2, proof of Theorem 1

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Read-back

Setting. Throughout, $\mathbb{R}$ is the field of real numbers with its usual ring structure and its usual topology (the one induced by the metric $d(x,y)=|x-y|$ ). A subring of $\mathbb{R}$ here means a subset that contains $0$ and $1$ and is closed under addition, negation and multiplication (subrings are unital: they always contain $1$ ).

The smallest subring of $\mathbb{R}$ is the set of integers

\mathbb{Z} = \{\, n\cdot 1 : n \in \mathbb{Z}\,\} \subseteq \mathbb{R},

i.e. the image of the canonical map $\mathbb{Z}\to\mathbb{R}$ . Every subring of $\mathbb{R}$ contains it.

Statement. Let $A$ be a subring of $\mathbb{R}$ , and assume

A \neq \mathbb{Z},

that is, $A$ is not the subring consisting of exactly the integers. (Since every subring contains $\mathbb{Z}$ , this is the same as saying that $A$ contains at least one real number that is not an integer.)

Then there exists a subring $A'$ of $\mathbb{R}$ such that all three of the following hold:

$A' \subseteq A$ (containment as sets, not necessarily proper; $A' = A$ is allowed);
$A'$ is countable, meaning there is an injective map $A' \to \mathbb{N}$ (finite sets would also qualify; neither finiteness nor infiniteness is stated);
$A'$ is dense in $\mathbb{R}$ : every real number lies in the closure of $A'$ , equivalently every nonempty open interval of $\mathbb{R}$ meets $A'$ .

Remarks on the quantifiers and edge cases.

The only hypothesis is $A \neq \mathbb{Z}$ ; there are no further assumptions on $A$ (it may be countable or uncountable, and may be all of $\mathbb{R}$ ).
The hypothesis is satisfiable (for example by $A = \mathbb{R}$ ), so it is not vacuous.
Nothing is asserted about uniqueness of $A'$ , about $A'$ being finitely generated, or about any relation between $A'$ and $A$ beyond $A' \subseteq A$ .

Human review

Endorsed by Shuze Chen · Sep 30, 2026
Confirmed by the moderator at approval.
Endorsed by dbenbenn · Sep 30, 2026
Confirmed by the mission captain (proposal self-audit).

View graph