spec — Mathlib

English

There is an explicit isomorphism taking the modular cyclotomic character to units in Z/nZ, compatible with group operations.

Русский

Существует явное изоморфирование, переводящее модулярный циклотомический характер в единицы Z/nZ и совместимое с групповой структурой.

LaTeX

$$$\\text{modularCyclotomicCharacter}'(L,n): Aut(L) \\to (\\mathbb{Z}/n\\mathbb{Z})^{\\times}$ is a monoid homomorphism into units$$

Lean4

theorem spec (g : L ≃+* L) {t : Lˣ} (ht : t ∈ rootsOfUnity n L) :
    g t = t ^ ((modularCyclotomicCharacter L hn g) : ZMod n).val :=
  by
  rw [toFun_spec' g ht]
  congr 1
  exact (ZMod.ringEquivCongr_val _ _).symm

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