toFun — Mathlib

English

The function toFun(n,g) records the exponent j in ZMod such that g(ζ) = ζ^j for all nth roots of unity ζ.

Русский

Функция toFun(n,g) фиксирует показатель j в ZMod, удовлетворяющий g(ζ) = ζ^j для всех ζ — n-й корень единства.

LaTeX

$$$\\text{toFun}(n,g) = j \\in \\mathbb{Z}/d\\mathbb{Z} \\text{ s.t. } g(ζ)=ζ^{j}$ для всех $ζ$ с $ζ^{n}=1$$$

Lean4

/-- If `g` is a ring automorphism of `L`, and `n : ℕ+`, then
  `modularCyclotomicCharacter.toFun n g` is the `j : ZMod d` such that `g(ζ)=ζ^j` for all
  `n`-th roots of unity. Here `d` is the number of `n`th roots of unity in `L`. -/
noncomputable def toFun (n : ℕ) [NeZero n] (g : L ≃+* L) : ZMod (Fintype.card (rootsOfUnity n L)) :=
  modularCyclotomicCharacter.aux g n

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