toFun_spec — Mathlib

English

Specifies that toFun(n,g) gives the exponent such that g acts on each nth root by raising to that power.

Русский

Указывает, что toFun(n,g) задаёт показатель, по которому g действует на каждый n-й корень, возводя в эту степень.

LaTeX

$$$\\forall t,\\; g(t) = t^{(toFun(n,g)).val}$, for t in rootsOfUnity(n,L)$$

Lean4

/-- The formula which characterises the output of `modularCyclotomicCharacter g n`. -/
theorem toFun_spec (g : L ≃+* L) {n : ℕ} [NeZero n] (t : rootsOfUnity n L) : g (t : Lˣ) = (t ^ (χ₀ n g).val : Lˣ) :=
  by
  rw [modularCyclotomicCharacter.aux_spec g n t, ← zpow_natCast, modularCyclotomicCharacter.toFun, ZMod.val_intCast, ←
    Subgroup.coe_zpow]
  exact Units.ext_iff.1 <| SetCoe.ext_iff.2 <| zpow_eq_zpow_emod _ pow_card_eq_one (G := rootsOfUnity n L)

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