Theorems · Definition · number theory

modularCyclotomicCharacter

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

Given a positive integer n and a field L containing n nth roots of unity, modularCyclotomicCharacter n is a multiplicative homomorphism from the automorphisms of L to (ℤ/nℤ)ˣ. It is uniquely characterised by the property that g(ζ)=ζ^(modularCyclotomicCharacter n g) for g an automorphism of L and ζ any nth root of unity.

Defined in

Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Cited by

6 results in Mathlib

Foundations

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

Assumes

CommRingIsDomainNeZero