toFun_apply — Mathlib

English

The ZModPow of the cyclotomic character coincides with the modular cyclotomic character composed with the natural map to ZMod.

Русский

ZModPow циклотомического символа совпадает с композицией модульного циклотомического символа и естественного отображения в ZMod.

LaTeX

$$$\\big(\\chi(p,g)\\big)^{\\!}_{\\mathrm{toZModPow}} = (\\text{modularCyclotomicCharacter}) g$$$

Lean4

theorem toFun_apply :
    cyclotomicCharacter.toFun p g =
      PadicInt.ofIntSeq _
        (PadicInt.isCauSeq_padicNorm_of_pow_dvd_sub (aux g <| p ^ ·) _ fun i ↦
          pow_dvd_aux_pow_sub_aux_pow g p i.le_succ) :=
  dif_pos fun _ ↦ HasEnoughRootsOfUnity.exists_primitiveRoot _ _

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