English
If g is an automorphism of L and c is an element of Z/(Fintype.card(rootsOfUnity n L)) such that g(t) = t^c for all t in the set of n-th roots of unity, then c equals χ₀(n,g).
Русский
Пусть g — автоморфизм L и c ∈ Z/(cardinality) такой, что для всех корней из единицы степени n верно g(t) = t^c, тогда c равно χ₀(n,g).
LaTeX
$$$\\forall g\\,\\forall c\\in \\mathbb{Z}/\\big(\\!\\!\\mathrm{card}(\\mathrm{rootsOfUnity}_n L)\\big)\\,\\big(\\forall t\\in \\mathrm{rootsOfUnity}_n L,\, g(t)=t^c\\big) \\Rightarrow c=\\chi_{0}(n,g)$$$
Lean4
/-- If g(t)=t^c for all roots of unity, then c=χ(g). -/
theorem toFun_unique (g : L ≃+* L) (c : ZMod (Fintype.card (rootsOfUnity n L)))
(hc : ∀ t : rootsOfUnity n L, g (t : Lˣ) = (t ^ c.val : Lˣ)) : c = χ₀ n g :=
by
apply IsCyclic.ext Nat.card_eq_fintype_card (fun ζ ↦ ?_)
specialize hc ζ
suffices ((ζ ^ c.val : Lˣ) : L) = (ζ ^ (χ₀ n g).val : Lˣ) by exact_mod_cast this
rw [← toFun_spec g ζ, hc]
