Documentation

Mathlib.RingTheory.RootsOfUnity.Basic

Roots of unity and primitive roots of unity #

We define roots of unity in the context of an arbitrary commutative monoid, as a subgroup of the group of units. We also define a predicate IsPrimitiveRoot on commutative monoids, expressing that an element is a primitive root of unity.

Main definitions #

Main results #

Implementation details #

It is desirable that rootsOfUnity is a subgroup, and it will mainly be applied to rings (e.g. the ring of integers in a number field) and fields. We therefore implement it as a subgroup of the units of a commutative monoid.

We have chosen to define rootsOfUnity n for n : ℕ+, instead of n : ℕ, because almost all lemmas need the positivity assumption, and in particular the type class instances for Fintype and IsCyclic.

On the other hand, for primitive roots of unity, it is desirable to have a predicate not just on units, but directly on elements of the ring/field. For example, we want to say that exp (2 * pi * I / n) is a primitive n-th root of unity in the complex numbers, without having to turn that number into a unit first.

This creates a little bit of friction, but lemmas like IsPrimitiveRoot.isUnit and IsPrimitiveRoot.coe_units_iff should provide the necessary glue.

def rootsOfUnity (k : ℕ+) (M : Type u_7) [CommMonoid M] :

rootsOfUnity k M is the subgroup of elements m : Mˣ that satisfy m ^ k = 1.

Equations
  • rootsOfUnity k M = { carrier := {ζ : Mˣ | ζ ^ k = 1}, mul_mem' := , one_mem' := , inv_mem' := }
Instances For
    @[simp]
    theorem mem_rootsOfUnity {M : Type u_1} [CommMonoid M] (k : ℕ+) (ζ : Mˣ) :
    ζ rootsOfUnity k M ζ ^ k = 1
    theorem mem_rootsOfUnity' {M : Type u_1} [CommMonoid M] (k : ℕ+) (ζ : Mˣ) :
    ζ rootsOfUnity k M ζ ^ k = 1
    @[simp]
    theorem rootsOfUnity_one (M : Type u_7) [CommMonoid M] :
    theorem rootsOfUnity.coe_injective {M : Type u_1} [CommMonoid M] {n : ℕ+} :
    Function.Injective fun (x : (rootsOfUnity n M)) => x
    @[simp]
    theorem rootsOfUnity.val_mkOfPowEq_coe {M : Type u_1} [CommMonoid M] (ζ : M) {n : ℕ+} (h : ζ ^ n = 1) :
    (rootsOfUnity.mkOfPowEq ζ h) = ζ
    def rootsOfUnity.mkOfPowEq {M : Type u_1} [CommMonoid M] (ζ : M) {n : ℕ+} (h : ζ ^ n = 1) :
    (rootsOfUnity n M)

    Make an element of rootsOfUnity from a member of the base ring, and a proof that it has a positive power equal to one.

    Equations
    Instances For
      @[simp]
      theorem rootsOfUnity.coe_mkOfPowEq {M : Type u_1} [CommMonoid M] {ζ : M} {n : ℕ+} (h : ζ ^ n = 1) :
      (rootsOfUnity.mkOfPowEq ζ h) = ζ
      theorem rootsOfUnity_le_of_dvd {M : Type u_1} [CommMonoid M] {k : ℕ+} {l : ℕ+} (h : k l) :
      theorem map_rootsOfUnity {M : Type u_1} {N : Type u_2} [CommMonoid M] [CommMonoid N] (f : Mˣ →* Nˣ) (k : ℕ+) :
      theorem rootsOfUnity.coe_pow {R : Type u_4} {k : ℕ+} [CommMonoid R] (ζ : (rootsOfUnity k R)) (m : ) :
      (ζ ^ m) = ζ ^ m
      def restrictRootsOfUnity {R : Type u_4} {S : Type u_5} {F : Type u_6} [CommMonoid R] [CommMonoid S] [FunLike F R S] [MonoidHomClass F R S] (σ : F) (n : ℕ+) :
      (rootsOfUnity n R) →* (rootsOfUnity n S)

      Restrict a ring homomorphism to the nth roots of unity.

      Equations
      Instances For
        @[simp]
        theorem restrictRootsOfUnity_coe_apply {R : Type u_4} {S : Type u_5} {F : Type u_6} {k : ℕ+} [CommMonoid R] [CommMonoid S] [FunLike F R S] [MonoidHomClass F R S] (σ : F) (ζ : (rootsOfUnity k R)) :
        ((restrictRootsOfUnity σ k) ζ) = σ ζ
        def MulEquiv.restrictRootsOfUnity {R : Type u_4} {S : Type u_5} [CommMonoid R] [CommMonoid S] (σ : R ≃* S) (n : ℕ+) :
        (rootsOfUnity n R) ≃* (rootsOfUnity n S)

        Restrict a monoid isomorphism to the nth roots of unity.

        Equations
        Instances For
          @[simp]
          theorem MulEquiv.restrictRootsOfUnity_coe_apply {R : Type u_4} {S : Type u_5} {k : ℕ+} [CommMonoid R] [CommMonoid S] (σ : R ≃* S) (ζ : (rootsOfUnity k R)) :
          ((σ.restrictRootsOfUnity k) ζ) = σ ζ
          @[simp]
          theorem MulEquiv.restrictRootsOfUnity_symm {R : Type u_4} {S : Type u_5} {k : ℕ+} [CommMonoid R] [CommMonoid S] (σ : R ≃* S) :
          (σ.restrictRootsOfUnity k).symm = σ.symm.restrictRootsOfUnity k
          theorem mem_rootsOfUnity_iff_mem_nthRoots {R : Type u_4} {k : ℕ+} [CommRing R] [IsDomain R] {ζ : Rˣ} :
          def rootsOfUnityEquivNthRoots (R : Type u_4) (k : ℕ+) [CommRing R] [IsDomain R] :
          (rootsOfUnity k R) { x : R // x Polynomial.nthRoots (k) 1 }

          Equivalence between the k-th roots of unity in R and the k-th roots of 1.

          This is implemented as equivalence of subtypes, because rootsOfUnity is a subgroup of the group of units, whereas nthRoots is a multiset.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[simp]
            theorem rootsOfUnityEquivNthRoots_apply {R : Type u_4} {k : ℕ+} [CommRing R] [IsDomain R] (x : (rootsOfUnity k R)) :
            ((rootsOfUnityEquivNthRoots R k) x) = x
            @[simp]
            theorem rootsOfUnityEquivNthRoots_symm_apply {R : Type u_4} {k : ℕ+} [CommRing R] [IsDomain R] (x : { x : R // x Polynomial.nthRoots (k) 1 }) :
            ((rootsOfUnityEquivNthRoots R k).symm x) = x
            instance rootsOfUnity.fintype (R : Type u_4) (k : ℕ+) [CommRing R] [IsDomain R] :
            Equations
            instance rootsOfUnity.isCyclic (R : Type u_4) (k : ℕ+) [CommRing R] [IsDomain R] :
            Equations
            • =
            theorem card_rootsOfUnity (R : Type u_4) (k : ℕ+) [CommRing R] [IsDomain R] :
            theorem map_rootsOfUnity_eq_pow_self {R : Type u_4} {F : Type u_6} {k : ℕ+} [CommRing R] [IsDomain R] [FunLike F R R] [RingHomClass F R R] (σ : F) (ζ : (rootsOfUnity k R)) :
            ∃ (m : ), σ ζ = ζ ^ m
            theorem mem_rootsOfUnity_prime_pow_mul_iff (R : Type u_4) [CommRing R] [IsReduced R] (p : ) (k : ) (m : ℕ+) [ExpChar R p] {ζ : Rˣ} :
            ζ rootsOfUnity (p, ^ k * m) R ζ rootsOfUnity m R
            @[simp]
            theorem mem_rootsOfUnity_prime_pow_mul_iff' (R : Type u_4) [CommRing R] [IsReduced R] (p : ) (k : ) (m : ℕ+) [ExpChar R p] {ζ : Rˣ} :
            ζ ^ (p ^ k * m) = 1 ζ rootsOfUnity m R
            theorem IsPrimitiveRoot.iff_def {M : Type u_1} [CommMonoid M] (ζ : M) (k : ) :
            IsPrimitiveRoot ζ k ζ ^ k = 1 ∀ (l : ), ζ ^ l = 1k l
            structure IsPrimitiveRoot {M : Type u_1} [CommMonoid M] (ζ : M) (k : ) :

            An element ζ is a primitive k-th root of unity if ζ ^ k = 1, and if l satisfies ζ ^ l = 1 then k ∣ l.

            • pow_eq_one : ζ ^ k = 1
            • dvd_of_pow_eq_one : ∀ (l : ), ζ ^ l = 1k l
            Instances For
              theorem IsPrimitiveRoot.pow_eq_one {M : Type u_1} [CommMonoid M] {ζ : M} {k : } (self : IsPrimitiveRoot ζ k) :
              ζ ^ k = 1
              theorem IsPrimitiveRoot.dvd_of_pow_eq_one {M : Type u_1} [CommMonoid M] {ζ : M} {k : } (self : IsPrimitiveRoot ζ k) (l : ) :
              ζ ^ l = 1k l
              @[simp]
              theorem IsPrimitiveRoot.val_toRootsOfUnity_coe {M : Type u_1} [CommMonoid M] {μ : M} {n : ℕ+} (h : IsPrimitiveRoot μ n) :
              h.toRootsOfUnity = μ
              @[simp]
              theorem IsPrimitiveRoot.val_inv_toRootsOfUnity_coe {M : Type u_1} [CommMonoid M] {μ : M} {n : ℕ+} (h : IsPrimitiveRoot μ n) :
              (h.toRootsOfUnity)⁻¹ = μ ^ (n - 1)
              def IsPrimitiveRoot.toRootsOfUnity {M : Type u_1} [CommMonoid M] {μ : M} {n : ℕ+} (h : IsPrimitiveRoot μ n) :
              (rootsOfUnity n M)

              Turn a primitive root μ into a member of the rootsOfUnity subgroup.

              Equations
              Instances For
                def primitiveRoots (k : ) (R : Type u_7) [CommRing R] [IsDomain R] :

                primitiveRoots k R is the finset of primitive k-th roots of unity in the integral domain R.

                Equations
                Instances For
                  @[simp]
                  theorem mem_primitiveRoots {R : Type u_4} {k : } [CommRing R] [IsDomain R] {ζ : R} (h0 : 0 < k) :
                  @[simp]
                  theorem isPrimitiveRoot_of_mem_primitiveRoots {R : Type u_4} {k : } [CommRing R] [IsDomain R] {ζ : R} (h : ζ primitiveRoots k R) :
                  theorem IsPrimitiveRoot.mk_of_lt {M : Type u_1} [CommMonoid M] {k : } (ζ : M) (hk : 0 < k) (h1 : ζ ^ k = 1) (h : ∀ (l : ), 0 < ll < kζ ^ l 1) :
                  theorem IsPrimitiveRoot.pow_eq_one_iff_dvd {M : Type u_1} [CommMonoid M] {k : } {ζ : M} (h : IsPrimitiveRoot ζ k) (l : ) :
                  ζ ^ l = 1 k l
                  theorem IsPrimitiveRoot.isUnit {M : Type u_1} [CommMonoid M] {k : } {ζ : M} (h : IsPrimitiveRoot ζ k) (h0 : 0 < k) :
                  theorem IsPrimitiveRoot.pow_ne_one_of_pos_of_lt {M : Type u_1} [CommMonoid M] {k : } {l : } {ζ : M} (h : IsPrimitiveRoot ζ k) (h0 : 0 < l) (hl : l < k) :
                  ζ ^ l 1
                  theorem IsPrimitiveRoot.ne_one {M : Type u_1} [CommMonoid M] {k : } {ζ : M} (h : IsPrimitiveRoot ζ k) (hk : 1 < k) :
                  ζ 1
                  theorem IsPrimitiveRoot.pow_inj {M : Type u_1} [CommMonoid M] {k : } {ζ : M} (h : IsPrimitiveRoot ζ k) ⦃i : ⦃j : (hi : i < k) (hj : j < k) (H : ζ ^ i = ζ ^ j) :
                  i = j
                  @[simp]
                  theorem IsPrimitiveRoot.one_right_iff {M : Type u_1} [CommMonoid M] {ζ : M} :
                  @[simp]
                  theorem IsPrimitiveRoot.coe_submonoidClass_iff {k : } {M : Type u_7} {B : Type u_8} [CommMonoid M] [SetLike B M] [SubmonoidClass B M] {N : B} {ζ : N} :
                  @[simp]
                  theorem IsPrimitiveRoot.coe_units_iff {M : Type u_1} [CommMonoid M] {k : } {ζ : Mˣ} :
                  theorem IsPrimitiveRoot.isUnit_unit {M : Type u_1} [CommMonoid M] {ζ : M} {n : } (hn : 0 < n) (hζ : IsPrimitiveRoot ζ n) :
                  IsPrimitiveRoot .unit n
                  theorem IsPrimitiveRoot.isUnit_unit' {G : Type u_3} [DivisionCommMonoid G] {ζ : G} {n : } (hn : 0 < n) (hζ : IsPrimitiveRoot ζ n) :
                  IsPrimitiveRoot .unit' n
                  theorem IsPrimitiveRoot.pow_of_coprime {M : Type u_1} [CommMonoid M] {k : } {ζ : M} (h : IsPrimitiveRoot ζ k) (i : ) (hi : i.Coprime k) :
                  theorem IsPrimitiveRoot.pow_of_prime {M : Type u_1} [CommMonoid M] {k : } {ζ : M} (h : IsPrimitiveRoot ζ k) {p : } (hprime : Nat.Prime p) (hdiv : ¬p k) :
                  theorem IsPrimitiveRoot.pow_iff_coprime {M : Type u_1} [CommMonoid M] {k : } {ζ : M} (h : IsPrimitiveRoot ζ k) (h0 : 0 < k) (i : ) :
                  IsPrimitiveRoot (ζ ^ i) k i.Coprime k
                  theorem IsPrimitiveRoot.orderOf {M : Type u_1} [CommMonoid M] (ζ : M) :
                  theorem IsPrimitiveRoot.unique {M : Type u_1} [CommMonoid M] {k : } {l : } {ζ : M} (hk : IsPrimitiveRoot ζ k) (hl : IsPrimitiveRoot ζ l) :
                  k = l
                  theorem IsPrimitiveRoot.eq_orderOf {M : Type u_1} [CommMonoid M] {k : } {ζ : M} (h : IsPrimitiveRoot ζ k) :
                  k = orderOf ζ
                  theorem IsPrimitiveRoot.iff {M : Type u_1} [CommMonoid M] {k : } {ζ : M} (hk : 0 < k) :
                  IsPrimitiveRoot ζ k ζ ^ k = 1 ∀ (l : ), 0 < ll < kζ ^ l 1
                  theorem IsPrimitiveRoot.not_iff {M : Type u_1} [CommMonoid M] {k : } {ζ : M} :
                  theorem IsPrimitiveRoot.pow_mul_pow_lcm {M : Type u_1} [CommMonoid M] {k : } {ζ : M} {ζ' : M} {k' : } (hζ : IsPrimitiveRoot ζ k) (hζ' : IsPrimitiveRoot ζ' k') (hk : k 0) (hk' : k' 0) :
                  IsPrimitiveRoot (ζ ^ (k / k.factorizationLCMLeft k') * ζ' ^ (k' / k.factorizationLCMRight k')) (k.lcm k')
                  theorem IsPrimitiveRoot.pow_of_dvd {M : Type u_1} [CommMonoid M] {k : } {ζ : M} (h : IsPrimitiveRoot ζ k) {p : } (hp : p 0) (hdiv : p k) :
                  IsPrimitiveRoot (ζ ^ p) (k / p)
                  theorem IsPrimitiveRoot.mem_rootsOfUnity {M : Type u_1} [CommMonoid M] {ζ : Mˣ} {n : ℕ+} (h : IsPrimitiveRoot ζ n) :
                  theorem IsPrimitiveRoot.pow {M : Type u_1} [CommMonoid M] {ζ : M} {n : } {a : } {b : } (hn : 0 < n) (h : IsPrimitiveRoot ζ n) (hprod : n = a * b) :

                  If there is an n-th primitive root of unity in R and b divides n, then there is a b-th primitive root of unity in R.

                  theorem IsPrimitiveRoot.injOn_pow {M : Type u_1} [CommMonoid M] {n : } {ζ : M} (hζ : IsPrimitiveRoot ζ n) :
                  Set.InjOn (fun (x : ) => ζ ^ x) (Finset.range n)
                  theorem IsPrimitiveRoot.map_of_injective {M : Type u_1} {N : Type u_2} {F : Type u_6} [CommMonoid M] [CommMonoid N] {k : } {ζ : M} {f : F} [FunLike F M N] [MonoidHomClass F M N] (h : IsPrimitiveRoot ζ k) (hf : Function.Injective f) :
                  theorem IsPrimitiveRoot.of_map_of_injective {M : Type u_1} {N : Type u_2} {F : Type u_6} [CommMonoid M] [CommMonoid N] {k : } {ζ : M} {f : F} [FunLike F M N] [MonoidHomClass F M N] (h : IsPrimitiveRoot (f ζ) k) (hf : Function.Injective f) :
                  theorem IsPrimitiveRoot.map_iff_of_injective {M : Type u_1} {N : Type u_2} {F : Type u_6} [CommMonoid M] [CommMonoid N] {k : } {ζ : M} {f : F} [FunLike F M N] [MonoidHomClass F M N] (hf : Function.Injective f) :
                  theorem IsPrimitiveRoot.ne_zero {k : } {M₀ : Type u_7} [CommMonoidWithZero M₀] [Nontrivial M₀] {ζ : M₀} (h : IsPrimitiveRoot ζ k) :
                  k 0ζ 0
                  theorem IsPrimitiveRoot.injOn_pow_mul {M₀ : Type u_7} [CancelCommMonoidWithZero M₀] {n : } {ζ : M₀} (hζ : IsPrimitiveRoot ζ n) {α : M₀} (hα : α 0) :
                  Set.InjOn (fun (x : ) => ζ ^ x * α) (Finset.range n)
                  theorem IsPrimitiveRoot.zpow_eq_one {G : Type u_3} [DivisionCommMonoid G] {k : } {ζ : G} (h : IsPrimitiveRoot ζ k) :
                  ζ ^ k = 1
                  theorem IsPrimitiveRoot.zpow_eq_one_iff_dvd {G : Type u_3} [DivisionCommMonoid G] {k : } {ζ : G} (h : IsPrimitiveRoot ζ k) (l : ) :
                  ζ ^ l = 1 k l
                  theorem IsPrimitiveRoot.inv {G : Type u_3} [DivisionCommMonoid G] {k : } {ζ : G} (h : IsPrimitiveRoot ζ k) :
                  @[simp]
                  theorem IsPrimitiveRoot.zpow_of_gcd_eq_one {G : Type u_3} [DivisionCommMonoid G] {k : } {ζ : G} (h : IsPrimitiveRoot ζ k) (i : ) (hi : i.gcd k = 1) :
                  theorem IsPrimitiveRoot.sub_one_ne_zero {R : Type u_4} [CommRing R] {n : } (hn : 1 < n) {ζ : R} (hζ : IsPrimitiveRoot ζ n) :
                  ζ - 1 0
                  theorem IsPrimitiveRoot.neZero' {R : Type u_4} {ζ : R} [CommRing R] [IsDomain R] {n : ℕ+} (hζ : IsPrimitiveRoot ζ n) :
                  NeZero n
                  theorem IsPrimitiveRoot.mem_nthRootsFinset {R : Type u_4} {k : } {ζ : R} [CommRing R] [IsDomain R] (hζ : IsPrimitiveRoot ζ k) (hk : 0 < k) :
                  theorem IsPrimitiveRoot.eq_neg_one_of_two_right {R : Type u_4} [CommRing R] [NoZeroDivisors R] {ζ : R} (h : IsPrimitiveRoot ζ 2) :
                  ζ = -1
                  theorem IsPrimitiveRoot.neg_one {R : Type u_4} [CommRing R] (p : ) [Nontrivial R] [h : CharP R p] (hp : p 2) :
                  theorem IsPrimitiveRoot.geom_sum_eq_zero {R : Type u_4} {k : } [CommRing R] [IsDomain R] {ζ : R} (hζ : IsPrimitiveRoot ζ k) (hk : 1 < k) :
                  iFinset.range k, ζ ^ i = 0

                  If 1 < k then (∑ i ∈ range k, ζ ^ i) = 0.

                  theorem IsPrimitiveRoot.pow_sub_one_eq {R : Type u_4} {k : } [CommRing R] [IsDomain R] {ζ : R} (hζ : IsPrimitiveRoot ζ k) (hk : 1 < k) :
                  ζ ^ k.pred = -iFinset.range k.pred, ζ ^ i

                  If 1 < k, then ζ ^ k.pred = -(∑ i ∈ range k.pred, ζ ^ i).

                  The (additive) monoid equivalence between ZMod k and the powers of a primitive root of unity ζ.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    @[simp]
                    theorem IsPrimitiveRoot.zmodEquivZPowers_apply_coe_int {R : Type u_4} {k : } [CommRing R] {ζ : Rˣ} (h : IsPrimitiveRoot ζ k) (i : ) :
                    h.zmodEquivZPowers i = Additive.ofMul ζ ^ i,
                    @[simp]
                    theorem IsPrimitiveRoot.zmodEquivZPowers_apply_coe_nat {R : Type u_4} {k : } [CommRing R] {ζ : Rˣ} (h : IsPrimitiveRoot ζ k) (i : ) :
                    h.zmodEquivZPowers i = Additive.ofMul ζ ^ i,
                    @[simp]
                    theorem IsPrimitiveRoot.zmodEquivZPowers_symm_apply_zpow {R : Type u_4} {k : } [CommRing R] {ζ : Rˣ} (h : IsPrimitiveRoot ζ k) (i : ) :
                    h.zmodEquivZPowers.symm (Additive.ofMul ζ ^ i, ) = i
                    @[simp]
                    theorem IsPrimitiveRoot.zmodEquivZPowers_symm_apply_zpow' {R : Type u_4} {k : } [CommRing R] {ζ : Rˣ} (h : IsPrimitiveRoot ζ k) (i : ) :
                    h.zmodEquivZPowers.symm ζ ^ i, = i
                    @[simp]
                    theorem IsPrimitiveRoot.zmodEquivZPowers_symm_apply_pow {R : Type u_4} {k : } [CommRing R] {ζ : Rˣ} (h : IsPrimitiveRoot ζ k) (i : ) :
                    h.zmodEquivZPowers.symm (Additive.ofMul ζ ^ i, ) = i
                    @[simp]
                    theorem IsPrimitiveRoot.zmodEquivZPowers_symm_apply_pow' {R : Type u_4} {k : } [CommRing R] {ζ : Rˣ} (h : IsPrimitiveRoot ζ k) (i : ) :
                    h.zmodEquivZPowers.symm ζ ^ i, = i
                    theorem IsPrimitiveRoot.zpowers_eq {R : Type u_4} [CommRing R] [IsDomain R] {k : ℕ+} {ζ : Rˣ} (h : IsPrimitiveRoot ζ k) :
                    theorem IsPrimitiveRoot.map_rootsOfUnity {R : Type u_4} [CommRing R] [IsDomain R] {S : Type u_7} {F : Type u_8} [CommRing S] [IsDomain S] [FunLike F R S] [MonoidHomClass F R S] {ζ : R} {n : ℕ+} (hζ : IsPrimitiveRoot ζ n) {f : F} (hf : Function.Injective f) :
                    theorem val_rootsOfUnityEquivOfPrimitiveRoots_apply_coe {R : Type u_4} [CommRing R] [IsDomain R] {S : Type u_7} {F : Type u_8} [CommRing S] [IsDomain S] [FunLike F R S] [MonoidHomClass F R S] {n : ℕ+} {f : F} (hf : Function.Injective f) (hζ : (primitiveRoots (n) R).Nonempty) :
                    ∀ (a : (rootsOfUnity n R)), ((rootsOfUnityEquivOfPrimitiveRoots hf ) a) = f a
                    theorem rootsOfUnityEquivOfPrimitiveRoots_apply_coe_inv_val {R : Type u_4} [CommRing R] [IsDomain R] {S : Type u_7} {F : Type u_8} [CommRing S] [IsDomain S] [FunLike F R S] [MonoidHomClass F R S] {n : ℕ+} {f : F} (hf : Function.Injective f) (hζ : (primitiveRoots (n) R).Nonempty) :
                    ∀ (a : (rootsOfUnity n R)), =
                    noncomputable def rootsOfUnityEquivOfPrimitiveRoots {R : Type u_4} [CommRing R] [IsDomain R] {S : Type u_7} {F : Type u_8} [CommRing S] [IsDomain S] [FunLike F R S] [MonoidHomClass F R S] {n : ℕ+} {f : F} (hf : Function.Injective f) (hζ : (primitiveRoots (n) R).Nonempty) :
                    (rootsOfUnity n R) ≃* (rootsOfUnity n S)

                    If R contains a 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.

                    Equations
                    Instances For
                      theorem rootsOfUnityEquivOfPrimitiveRoots_symm_apply {R : Type u_4} [CommRing R] [IsDomain R] {S : Type u_7} {F : Type u_8} [CommRing S] [IsDomain S] [FunLike F R S] [MonoidHomClass F R S] {n : ℕ+} {f : F} (hf : Function.Injective f) (hζ : (primitiveRoots (n) R).Nonempty) (η : (rootsOfUnity n S)) :
                      f ((rootsOfUnityEquivOfPrimitiveRoots hf ).symm η) = η
                      theorem IsPrimitiveRoot.eq_pow_of_mem_rootsOfUnity {R : Type u_4} [CommRing R] [IsDomain R] {k : ℕ+} {ζ : Rˣ} {ξ : Rˣ} (h : IsPrimitiveRoot ζ k) (hξ : ξ rootsOfUnity k R) :
                      i < k, ζ ^ i = ξ
                      theorem IsPrimitiveRoot.eq_pow_of_mem_rootsOfUnity' {R : Type u_4} [CommRing R] [IsDomain R] {k : } (hk : 0 < k) {ζ : R} (hζ : IsPrimitiveRoot ζ k) {ξ : Rˣ} (hξ : ξ rootsOfUnity k, hk R) :
                      i < k, ζ ^ i = ξ

                      A version of IsPrimitiveRoot.eq_pow_of_mem_rootsOfUnity that takes a natural number k as argument instead of a PNat (and ζ : R instead of ζ : Rˣ).

                      theorem IsPrimitiveRoot.eq_pow_of_pow_eq_one {R : Type u_4} [CommRing R] [IsDomain R] {k : } {ζ : R} {ξ : R} (h : IsPrimitiveRoot ζ k) (hξ : ξ ^ k = 1) (h0 : 0 < k) :
                      i < k, ζ ^ i = ξ
                      theorem IsPrimitiveRoot.isPrimitiveRoot_iff' {R : Type u_4} [CommRing R] [IsDomain R] {k : ℕ+} {ζ : Rˣ} {ξ : Rˣ} (h : IsPrimitiveRoot ζ k) :
                      IsPrimitiveRoot ξ k i < k, i.Coprime k ζ ^ i = ξ
                      theorem IsPrimitiveRoot.isPrimitiveRoot_iff {R : Type u_4} [CommRing R] [IsDomain R] {k : } {ζ : R} {ξ : R} (h : IsPrimitiveRoot ζ k) (h0 : 0 < k) :
                      IsPrimitiveRoot ξ k i < k, i.Coprime k ζ ^ i = ξ
                      theorem IsPrimitiveRoot.nthRoots_eq {R : Type u_4} [CommRing R] [IsDomain R] {n : } {ζ : R} (hζ : IsPrimitiveRoot ζ n) {α : R} {a : R} (e : α ^ n = a) :
                      Polynomial.nthRoots n a = Multiset.map (fun (x : ) => ζ ^ x * α) (Multiset.range n)
                      theorem IsPrimitiveRoot.card_nthRoots {R : Type u_4} [CommRing R] [IsDomain R] {n : } {ζ : R} (hζ : IsPrimitiveRoot ζ n) (a : R) :
                      Multiset.card (Polynomial.nthRoots n a) = if ∃ (α : R), α ^ n = a then n else 0
                      theorem IsPrimitiveRoot.card_rootsOfUnity' {R : Type u_4} [CommRing R] {ζ : Rˣ} [IsDomain R] {n : ℕ+} (h : IsPrimitiveRoot ζ n) :
                      theorem IsPrimitiveRoot.card_rootsOfUnity {R : Type u_4} [CommRing R] [IsDomain R] {ζ : R} {n : ℕ+} (h : IsPrimitiveRoot ζ n) :
                      theorem IsPrimitiveRoot.card_nthRoots_one {R : Type u_4} [CommRing R] [IsDomain R] {ζ : R} {n : } (h : IsPrimitiveRoot ζ n) :
                      Multiset.card (Polynomial.nthRoots n 1) = n

                      The cardinality of the multiset nthRoots ↑n (1 : R) is n if there is a primitive root of unity in R.

                      theorem IsPrimitiveRoot.nthRoots_nodup {R : Type u_4} [CommRing R] [IsDomain R] {ζ : R} {n : } (h : IsPrimitiveRoot ζ n) {a : R} (ha : a 0) :
                      theorem IsPrimitiveRoot.nthRoots_one_nodup {R : Type u_4} [CommRing R] [IsDomain R] {ζ : R} {n : } (h : IsPrimitiveRoot ζ n) :

                      The multiset nthRoots ↑n (1 : R) has no repeated elements if there is a primitive root of unity in R.

                      @[simp]
                      theorem IsPrimitiveRoot.card_nthRootsFinset {R : Type u_4} [CommRing R] [IsDomain R] {ζ : R} {n : } (h : IsPrimitiveRoot ζ n) :
                      theorem IsPrimitiveRoot.card_primitiveRoots {R : Type u_4} [CommRing R] [IsDomain R] {ζ : R} {k : } (h : IsPrimitiveRoot ζ k) :
                      (primitiveRoots k R).card = k.totient

                      If an integral domain has a primitive k-th root of unity, then it has φ k of them.

                      theorem IsPrimitiveRoot.disjoint {R : Type u_4} [CommRing R] [IsDomain R] {k : } {l : } (h : k l) :

                      The sets primitiveRoots k R are pairwise disjoint.

                      theorem IsPrimitiveRoot.nthRoots_one_eq_biUnion_primitiveRoots' {R : Type u_4} [CommRing R] [IsDomain R] {ζ : R} {n : ℕ+} (h : IsPrimitiveRoot ζ n) :
                      Polynomial.nthRootsFinset (n) R = (n).divisors.biUnion fun (i : ) => primitiveRoots i R

                      nthRoots n as a Finset is equal to the union of primitiveRoots i R for i ∣ n if there is a primitive root of unity in R. This holds for any Nat, not just PNat, see nthRoots_one_eq_bUnion_primitive_roots.

                      theorem IsPrimitiveRoot.nthRoots_one_eq_biUnion_primitiveRoots {R : Type u_4} [CommRing R] [IsDomain R] {ζ : R} {n : } (h : IsPrimitiveRoot ζ n) :
                      Polynomial.nthRootsFinset n R = n.divisors.biUnion fun (i : ) => primitiveRoots i R

                      nthRoots n as a Finset is equal to the union of primitiveRoots i R for i ∣ n if there is a primitive root of unity in R.

                      noncomputable def IsPrimitiveRoot.autToPow (R : Type u_4) {S : Type u_5} [CommRing S] [IsDomain S] {μ : S} {n : ℕ+} (hμ : IsPrimitiveRoot μ n) [CommRing R] [Algebra R S] :
                      (S ≃ₐ[R] S) →* (ZMod n)ˣ

                      The MonoidHom that takes an automorphism to the power of μ that μ gets mapped to under it.

                      Equations
                      • IsPrimitiveRoot.autToPow R = let μ' := .toRootsOfUnity; let_fun ho := ; { toFun := fun (σ : S ≃ₐ[R] S) => .choose, map_one' := , map_mul' := }.toHomUnits
                      Instances For
                        theorem IsPrimitiveRoot.coe_autToPow_apply (R : Type u_4) {S : Type u_5} [CommRing S] [IsDomain S] {μ : S} {n : ℕ+} (hμ : IsPrimitiveRoot μ n) [CommRing R] [Algebra R S] (f : S ≃ₐ[R] S) :
                        ((IsPrimitiveRoot.autToPow R ) f) = .choose
                        @[simp]
                        theorem IsPrimitiveRoot.autToPow_spec (R : Type u_4) {S : Type u_5} [CommRing S] [IsDomain S] {μ : S} {n : ℕ+} (hμ : IsPrimitiveRoot μ n) [CommRing R] [Algebra R S] (f : S ≃ₐ[R] S) :
                        μ ^ (((IsPrimitiveRoot.autToPow R ) f)).val = f μ