\(\widehat{\mathbb{Q}}\) and tensor products.

The definition of \(\widehat{\mathbb{Q}}\) is easy if you know about tensor products of additive abelian groups.

DefinitionQHat#

The profinite completion \(\widehat{\mathbb{Q}}\) of \(\mathbb{Q}\) is the tensor product \(\mathbb{Q}\otimes_{\mathbb{Z}}\widehat{\mathbb{Z}}\), or \(\widehat{\mathbb{Q}}=\mathbb{Q}\otimes\widehat{\mathbb{Z}}\) for short.

Lean

Formalized as QHat.

Sources
LeanQHat
Uses 1 · Used by 8
Statement usesZHat
Used byQHat.canonicalForm · QHat.injective_rat · QHat.injective_zHat · QHat.rat_join_zHat · QHat.rat_meet_zHat · QHat.unitsrat_join_unitszHat · Qhat.unitsrat_meet_unitszHat · HurwitzRatHat.canonicalForm

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.