Sanity check: the absolute Galois group of ℚ₂ is expressible with current Mathlib. Field.absoluteGaloisGroup K := AlgebraicClosure K ≃ₐ[K] AlgebraicClosure K, which for the characteristic-0 field ℚ₂ is the genuine Gal(ℚ₂^sep/ℚ₂) = G_{ℚ₂}.

@[reducible, inline]

noncomputable abbrev GQ2 : Type

G_{ℚ₂}, the absolute Galois group of the 2-adic numbers.

Equations

• GQ2 = Field.absoluteGaloisGroup ℚ_[2]