Theorems · Theorem · number theory

IsPrimitiveRoot.autToPow_eq_modularCyclotomicCharacter

∀ {L : Type u} [inst : CommRing L] [inst_1 : IsDomain L] (n : ℕ) [inst_2 : NeZero n] (R : Type u_1)
  [inst_3 : CommRing R] [inst_4 : Algebra R L] {μ : L} (hμ : IsPrimitiveRoot μ n) (g : L ≃ₐ[R] L),
  (IsPrimitiveRoot.autToPow R hμ) g = (modularCyclotomicCharacter L ⋯) g.toRingEquiv

The relationship between IsPrimitiveRoot.autToPow and modularCyclotomicCharacter. Note that IsPrimitiveRoot.autToPow needs an explicit root of unity, and also an auxiliary "base ring" R.

Defined in

Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingIsDomainNeZeroCommRingAlgebra