The finite adeles of the rationals.

Mathlib already has the definition of the finite adeles \(\mathbb{A}_{\mathbb{Q}}^f\) of the rationals as a commutative \(\mathbb{Q}\)-algebra, and the proof that it's a topological ring.

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.