Theorems · Definition · number theory

cyclotomicCharacter

(L : Type u) → [inst : CommRing L] → [IsDomain L] → (p : ℕ) → [inst_2 : Fact (Nat.Prime p)] → (L ≃+* L) →* ℤ_[p]ˣ

Suppose L is a domain containing all pⁱ-th primitive roots with p a (rational) prime. If g is a ring automorphism of L, then cyclotomicCharacter L p g is the unique j : ℤₚ such that g(ζ) = ζ ^ (j mod pⁱ) for all pⁱ-th roots of unity ζ. Note: This is the trivial character when L does not contain all pⁱ-th primitive roots.

Defined in

Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommRingIsDomainFact