toZModPow — Mathlib

English

There is a precise equality between the ZModPow representation of the cyclotomic character and the modular cyclotomic character composition.

Русский

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

LaTeX

$$$(\\chi p g).toZModPow n = (modularCyclotomicCharacter _ (Fintype.card_eq_nat_card.trans (HasEnoughRootsOfUnity.natCard_rootsOfUnity L (p^n))) g).val$$$

Lean4

theorem toZModPow (p : ℕ) [Fact p.Prime] {n : ℕ} [∀ i, HasEnoughRootsOfUnity L (p ^ i)] (g : L ≃+* L) :
    (cyclotomicCharacter L p g).val.toZModPow n =
      (modularCyclotomicCharacter _
          (Fintype.card_eq_nat_card.trans (HasEnoughRootsOfUnity.natCard_rootsOfUnity L (p ^ n))) g).val :=
  toZModPow_toFun _ _ _

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