Theorems · Definition · number theory

IsPrimitiveRoot.embeddingsEquivPrimitiveRoots

{n : ℕ} →
  [NeZero n] →
    {K : Type u} →
      {L : Type v} →
        [inst : Field K] →
          [inst_1 : CommRing L] →
            [IsDomain L] →
              [inst_3 : Algebra K L] →
                [IsCyclotomicExtension {n} K L] →
                  {ζ : L} →
                    IsPrimitiveRoot ζ n →
                      (C : Type u_1) →
                        [inst_5 : CommRing C] →
                          [inst_6 : IsDomain C] →
                            [inst_7 : Algebra K C] →
                              Irreducible (Polynomial.cyclotomic n K) → (L →ₐ[K] C) ≃ ↥(primitiveRoots n C)

The equivalence between L →ₐ[K] C and primitiveRoots n C given by a primitive root ζ.

Defined in

Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Cited by

3 results in Mathlib

Foundations

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

Assumes

NeZeroFieldCommRingIsDomainAlgebraIsCyclotomicExtensionCommRingIsDomainAlgebra