toZModPow_toFun — Mathlib

English

For units t in rootsOfUnity, g(t) equals t raised to the exponent given by modularCyclotomicCharacter'(L,n,g).

Русский

Для единиц t в корнях единицы: g(t) = t^{exponent}, где exponent задан модульной циклотомической характеристикой'

LaTeX

$$$g t = t^{ ((\\text{modularCyclotomicCharacter}' L n g)) : ZMod (Fintype.card { x // x \\in rootsOfUnity n L }) }.$$$

Lean4

theorem toZModPow_toFun (n : ℕ) :
    (χ p g).toZModPow n =
      (modularCyclotomicCharacter _
          (Fintype.card_eq_nat_card.trans (HasEnoughRootsOfUnity.natCard_rootsOfUnity L (p ^ n))) g).val :=
  by
  rw [toFun_apply]
  refine
    (PadicInt.toZModPow_ofIntSeq_of_pow_dvd_sub (aux g <| p ^ ·) _ (fun i ↦ pow_dvd_aux_pow_sub_aux_pow g p i.le_succ)
          n).trans
      ?_
  simp [modularCyclotomicCharacter, modularCyclotomicCharacter', modularCyclotomicCharacter.toFun]

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