English
There is a canonical isomorphism: Gal(L/K) ≅ Z/nZ, provided the hypotheses, via autEquivRootsOfUnity and its transfer to additive/multiplicative structure.
Русский
Существует каноническое изоморождение: Гал(L/K) ≅ Z/nZ через авт Equiv Roots Of Unity.
LaTeX
$$$\mathrm{Gal}(L/K) \cong \mathbb{Z}/n\mathbb{Z}.$$$
Lean4
/-- Suppose `L/K` is the splitting field of `Xⁿ - a`, and `ζ` is a `n`-th primitive root of unity
in `K`, then `Gal(L/K)` is isomorphic to `ZMod n`. -/
noncomputable def autEquivZmod [NeZero n] {ζ : K} (hζ : IsPrimitiveRoot ζ n) : (L ≃ₐ[K] L) ≃* Multiplicative (ZMod n) :=
haveI hn := Nat.pos_iff_ne_zero.mpr (ne_zero_of_irreducible_X_pow_sub_C H)
(autEquivRootsOfUnity ⟨ζ, (mem_primitiveRoots hn).mpr hζ⟩ H L).trans
((MulEquiv.subgroupCongr (IsPrimitiveRoot.zpowers_eq (hζ.isUnit_unit' hn.ne')).symm).trans
(hζ.isUnit_unit' hn.ne').zmodEquivZPowers.symm.toMultiplicativeRight)
