Theorems · Definition · number theory

modularCyclotomicCharacter.aux

{L : Type u} → [inst : CommRing L] → [IsDomain L] → L ≃+* L → (n : ℕ) → [NeZero n] → ℤ

modularCyclotomicCharacter_aux g n is a non-canonical auxiliary integer j, only well-defined modulo the number of n-th roots of unity in L, such that g(ζ)=ζ^j for all n-th roots of unity ζ in L.

Defined in

Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Cited by

7 results in Mathlib

Foundations

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

Assumes

CommRingIsDomainNeZero