English
There is a canonical automorphism of the cyclotomic extension carrying the primitive root ζ to any given primitive root μ, realized via the FromZetaAut construction.
Русский
Существует канонический автоморфизм циклотомического расширения, переводящий примитивный корень ζ в заданный примитивный корень μ, реализованный через конструкцию FromZetaAut.
LaTeX
$$$\text{fromZetaAut}\; h_\mu\; h = \text{(алгебра AUT, отправляющий } ζ \mapsto μ\text{)}$$$
Lean4
/-- Maps `μ` to the `AlgEquiv` that sends `IsCyclotomicExtension.zeta` to `μ`. -/
noncomputable def fromZetaAut : L ≃ₐ[K] L :=
let hζ := (zeta_spec n K L).eq_pow_of_pow_eq_one hμ.pow_eq_one
(autEquivPow L h).symm <|
ZMod.unitOfCoprime hζ.choose <|
((zeta_spec n K L).pow_iff_coprime (NeZero.pos _) hζ.choose).mp <| hζ.choose_spec.2.symm ▸ hμ
