Theorems · Theorem · number theory

cyclotomicCharacter.toZModPow

∀ {L : Type u} [inst : CommRing L] [inst_1 : IsDomain L] (p : ℕ) [inst_2 : Fact (Nat.Prime p)] {n : ℕ}
  [inst_3 : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)] (g : L ≃+* L),
  (PadicInt.toZModPow n) ↑((cyclotomicCharacter L p) g) = ↑((modularCyclotomicCharacter L ⋯) g)

Defined in

Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Cited by

1 results in Mathlib

Foundations

Depth 211 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingIsDomainFactHasEnoughRootsOfUnity