English
The function underlying the cyclotomic character on an automorphism is given by a PadicInt power sequence on primitive roots of unity.
Русский
Функция, лежащая в основе циклотомического характера, действует на примитивные корни через последовательность степеней в PadicInt.
LaTeX
$$$\\big(\\chi\\, p\\, g\\big) = \\text{PadicInt power sequence on primitive roots}$$$
Lean4
/-- The underlying function of the cyclotomic character. See `cyclotomicCharacter`. -/
noncomputable def toFun (p : ℕ) [Fact p.Prime] (g : L ≃+* L) : ℤ_[p] :=
if H : ∀ (i : ℕ), ∃ ζ : L, IsPrimitiveRoot ζ (p ^ i) then
haveI _ (i) : HasEnoughRootsOfUnity L (p ^ i) := ⟨H i, rootsOfUnity.isCyclic _ _⟩
PadicInt.ofIntSeq _
(PadicInt.isCauSeq_padicNorm_of_pow_dvd_sub (aux g <| p ^ ·) _ fun i ↦ pow_dvd_aux_pow_sub_aux_pow g p i.le_succ)
else 1
