Theorems · Theorem · number theory

modularCyclotomicCharacter.toFun_unique

∀ {L : Type u} [inst : CommRing L] [inst_1 : IsDomain L] (n : ℕ) [inst_2 : NeZero n] (g : L ≃+* L)
  (c : ZMod (Nat.card ↥(rootsOfUnity n L))),
  (∀ (t : ↥(rootsOfUnity n L)), g ↑↑t = ↑(↑t ^ c.val)) → c = modularCyclotomicCharacter.toFun n g

If g(t)=t^c for all roots of unity, then c=χ(g).

Defined in

Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommRingIsDomainNeZero