Theorems · Definition · number theory

IsPrimitiveRoot.adjoinEquivRingOfIntegersOfPrimePow

{p k : ℕ} →
  {K : Type u} →
    [inst : Field K] →
      {ζ : K} →
        [hp : Fact (Nat.Prime p)] →
          [inst_1 : CharZero K] →
            [IsCyclotomicExtension {p ^ k} ℚ K] → IsPrimitiveRoot ζ (p ^ k) → ↥ℤ[ζ] ≃ₐ[ℤ] NumberField.RingOfIntegers K

The algebra isomorphism adjoin ℤ {ζ} ≃ₐ[ℤ] (𝓞 K), where ζ is a primitive p ^ k-th root of unity and K is a p ^ k-th cyclotomic extension of ℚ.

Defined in

Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Cited by

5 results in Mathlib

Foundations

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

Assumes

FieldFactCharZeroIsCyclotomicExtension