English
The specialized version of fromZetaAut applied to the cyclotomic ζ shows that the induced automorphism maps to the primitive root μ exactly as prescribed by the isomorphism.
Русский
Специализированная версия fromZetaAut применительно к циклотомическому ζ показывает, что индуцированный автоморфизм отправляет примитивный корень μ точно так, как предписано изоморфизмом.
LaTeX
$$$\text{fromZetaAut}\; h_\mu\; h = \text{алг. образ, отправляющий } ζ \text{ в } μ$$$
Lean4
/-- `IsCyclotomicExtension.autEquivPow` repackaged in terms of `Gal`.
Asserts that the Galois group of `cyclotomic n K` is equivalent to `(ZMod n)ˣ`
if `cyclotomic n K` is irreducible in the base field. -/
noncomputable def galCyclotomicEquivUnitsZMod : (cyclotomic n K).Gal ≃* (ZMod n)ˣ :=
(AlgEquiv.autCongr (IsSplittingField.algEquiv L _ : L ≃ₐ[K] (cyclotomic n K).SplittingField)).symm.trans
(IsCyclotomicExtension.autEquivPow L h)
