toFun_unique' — Mathlib

English

If g is an automorphism and c is such that g(t) = t^c for all t ∈ rootsOfUnity n L (viewed as units), then c = χ₀(n,g).

Русский

Пусть g — автоморфизм, и если g(t) = t^c для всех t ∈ rootsOfUnity n L (как элементы группы единиц), то c = χ₀(n,g).

LaTeX

$$$\\forall t\\in \\mathrm{rootsOfUnity}_n L,\\; g(t)=t^c \\implies c=\\chi_{0}(n,g)$$$

Lean4

theorem toFun_unique' (g : L ≃+* L) (c : ZMod (Fintype.card (rootsOfUnity n L)))
    (hc : ∀ t ∈ rootsOfUnity n L, g t = t ^ c.val) : c = χ₀ n g :=
  toFun_unique n g c (fun ⟨_, ht⟩ ↦ hc _ ht)

Похожие утверждения