Theorems · Theorem · number theory

cyclotomicCharacter.toFun_spec

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

Defined in

Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingIsDomainFactHasEnoughRootsOfUnity