Theorems · Definition · number theory

rootsOfUnityEquivOfPrimitiveRoots

{R : Type u_4} →
  [inst : CommRing R] →
    [inst_1 : IsDomain R] →
      {S : Type u_7} →
        {F : Type u_8} →
          [inst_2 : CommRing S] →
            [IsDomain S] →
              [inst_4 : FunLike F R S] →
                [MonoidHomClass F R S] →
                  {n : ℕ} →
                    [NeZero n] →
                      {f : F} →
                        Function.Injective ⇑f →
                          (primitiveRoots n R).Nonempty → ↥(rootsOfUnity n R) ≃* ↥(rootsOfUnity n S)

If R contains an n-th primitive root, and S/R is a ring extension, then the n-th roots of unity in R and S are isomorphic. Also see IsPrimitiveRoot.map_rootsOfUnity for the equality as Subgroup Sˣ.

Defined in

Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Cited by

5 results in Mathlib

Foundations

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

Assumes

CommRingIsDomainCommRingIsDomainFunLikeMonoidHomClassNeZero