Theorems · Definition · number theory

modularCyclotomicCharacter.toFun

{L : Type u} → [inst : CommRing L] → [IsDomain L] → (n : ℕ) → [NeZero n] → L ≃+* L → ZMod (Nat.card ↥(rootsOfUnity n L))

If g is a ring automorphism of L, and n : ℕ+, then modularCyclotomicCharacter.toFun n g is the j : ZMod d such that g(ζ)=ζ^j for all n-th roots of unity. Here d is the number of nth roots of unity in L.

Defined in

Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Cited by

10 results in Mathlib

Foundations

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

Assumes

CommRingIsDomainNeZero