Theorems · Definition · number theory

IsPrimitiveRoot.adjoinEquivRingOfIntegers

{n : ℕ} →
  {K : Type u} →
    [inst : Field K] →
      {ζ : K} →
        [NeZero n] →
          [inst_2 : CharZero K] →
            [IsCyclotomicExtension {n} ℚ K] → IsPrimitiveRoot ζ n → ↥ℤ[ζ] ≃ₐ[ℤ] NumberField.RingOfIntegers K

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

Defined in

Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Cited by

5 results in Mathlib

Foundations

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

Assumes

FieldNeZeroCharZeroIsCyclotomicExtension