English
There is a Galois group isomorphism for the polynomial X^n − 1 over K with a choice of primitive root, identifying automorphisms with units in Z/nZ.
Русский
Для X^n−1 над K существует изоморфизм Галуа, который сопоставляет автоморфизм единице в Z/nZ.
LaTeX
$$$(\mathrm{Gal}(X^n-1/K)) \cong (\mathbb{Z}/n\mathbb{Z})^{\times}$$$
Lean4
/-- `IsCyclotomicExtension.autEquivPow` repackaged in terms of `Gal`.
Asserts that the Galois group of `X ^ n - 1` is equivalent to `(ZMod n)ˣ`
if `cyclotomic n K` is irreducible in the base field. -/
noncomputable def galXPowEquivUnitsZMod : (X ^ n - 1 : K[X]).Gal ≃* (ZMod n)ˣ :=
(AlgEquiv.autCongr (IsSplittingField.algEquiv L _ : L ≃ₐ[K] (X ^ n - 1 : K[X]).SplittingField)).symm.trans
(IsCyclotomicExtension.autEquivPow L h)
