Theorems · Theorem · number theory

cyclotomicCharacter.spec

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

Defined in

Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingIsDomainFactHasEnoughRootsOfUnity