English
For a chosen primitive root ζ and automorphism σ, autEquivRootsOfUnity acts so that autEquivRootsOfUnity hζ H L σ · α = σ α.
Русский
Для выбранного корня ζ и автоморфизма σ выполняется: autEquivRootsOfUnity hζ H L σ · α = σ α.
LaTeX
$$$\text{autEquivRootsOfUnity}(hζ,H,L)\,σ\,· α = σ(α).$$$
Lean4
theorem autEquivRootsOfUnity_smul [NeZero n] (σ : L ≃ₐ[K] L) : autEquivRootsOfUnity hζ H L σ • α = σ α :=
by
have ⟨ζ, hζ'⟩ := hζ
have hn := NeZero.pos n
rw [mem_primitiveRoots hn] at hζ'
rw [← mem_nthRoots hn,
(hζ'.map_of_injective (algebraMap K L).injective).nthRoots_eq (rootOfSplitsXPowSubC_pow a L)] at hα
simp only [Multiset.mem_map, Multiset.mem_range] at hα
obtain ⟨i, _, rfl⟩ := hα
simp only [← map_pow, ← Algebra.smul_def, map_smul, autEquivRootsOfUnity_apply_rootOfSplit hζ H L]
exact smul_comm _ _ _
