unique — Mathlib

English

If two exponents c,c′ give the same action on all roots of unity, then c=c′, i.e., the exponent is unique for a given automorphism.

Русский

Если два показателя дают одинаковое действие на все корни единства, то они равны между собой.

LaTeX

$$$\\forall c,c',\\; (\\forall t\\in \\mathrm{rootsOfUnity}_n L,\\ t^c=t^{c'}) \\Rightarrow c=c'$$$

Lean4

theorem unique (g : L ≃+* L) {c : ZMod n} (hc : ∀ t ∈ rootsOfUnity n L, g t = t ^ c.val) :
    c = modularCyclotomicCharacter L hn g :=
  by
  change c = (ZMod.ringEquivCongr hn) (toFun n g)
  rw [← toFun_unique' n g (ZMod.ringEquivCongr hn.symm c) (fun t ht ↦ by rw [hc t ht, ZMod.ringEquivCongr_val]), ←
    ZMod.ringEquivCongr_symm hn, RingEquiv.apply_symm_apply]

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