Documentation

Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Primitive roots in cyclotomic fields #

If IsCyclotomicExtension {n} A B, we define an element zeta n A B : B that is a primitive nth-root of unity in B and we study its properties. We also prove related theorems under the more general assumption of just being a primitive root, for reasons described in the implementation details section.

Main definitions #

Main results #

Implementation details #

zeta n A B is defined as any primitive root of unity in B, - this must exist, by definition of IsCyclotomicExtension. It is not true in general that it is a root of cyclotomic n B, but this holds if isDomain B and NeZero (↑n : B).

zeta n A B is defined using Exists.choose, which means we cannot control it. For example, in normal mathematics, we can demand that (zeta p ℤ ℤ[ζₚ] : ℚ(ζₚ)) is equal to zeta p ℚ ℚ(ζₚ), as we are just choosing "an arbitrary primitive root" and we can internally specify that our choices agree. This is not the case here, and it is indeed impossible to prove that these two are equal. Therefore, whenever possible, we prove our results for any primitive root, and only at the "final step", when we need to provide an "explicit" primitive root, we use zeta.

noncomputable def IsCyclotomicExtension.zeta (n : ℕ+) (A : Type w) (B : Type z) [CommRing A] [CommRing B] [Algebra A B] [IsCyclotomicExtension {n} A B] :
B

If B is an n-th cyclotomic extension of A, then zeta n A B is a primitive root of unity in B.

Equations
Instances For
    @[simp]

    zeta n A B is a primitive n-th root of unity.

    theorem IsCyclotomicExtension.zeta_isRoot (n : ℕ+) (A : Type w) (B : Type z) [CommRing A] [CommRing B] [Algebra A B] [IsCyclotomicExtension {n} A B] [IsDomain B] [NeZero n] :
    @[simp]
    theorem IsPrimitiveRoot.powerBasis_dim {n : ℕ+} (K : Type u) {L : Type v} [Field K] [CommRing L] [IsDomain L] [Algebra K L] [IsCyclotomicExtension {n} K L] {ζ : L} (hζ : IsPrimitiveRoot ζ n) :
    (IsPrimitiveRoot.powerBasis K ).dim = (minpoly K ζ).natDegree
    @[simp]
    theorem IsPrimitiveRoot.powerBasis_gen {n : ℕ+} (K : Type u) {L : Type v} [Field K] [CommRing L] [IsDomain L] [Algebra K L] [IsCyclotomicExtension {n} K L] {ζ : L} (hζ : IsPrimitiveRoot ζ n) :
    noncomputable def IsPrimitiveRoot.powerBasis {n : ℕ+} (K : Type u) {L : Type v} [Field K] [CommRing L] [IsDomain L] [Algebra K L] [IsCyclotomicExtension {n} K L] {ζ : L} (hζ : IsPrimitiveRoot ζ n) :

    The PowerBasis given by a primitive root η.

    Equations
    Instances For
      @[simp]
      theorem IsPrimitiveRoot.subOnePowerBasis_dim {n : ℕ+} (K : Type u) {L : Type v} [Field K] [CommRing L] [IsDomain L] [Algebra K L] [IsCyclotomicExtension {n} K L] {ζ : L} (hζ : IsPrimitiveRoot ζ n) :
      (IsPrimitiveRoot.subOnePowerBasis K ).dim = (minpoly K (ζ - 1)).natDegree
      @[simp]
      theorem IsPrimitiveRoot.subOnePowerBasis_gen {n : ℕ+} (K : Type u) {L : Type v} [Field K] [CommRing L] [IsDomain L] [Algebra K L] [IsCyclotomicExtension {n} K L] {ζ : L} (hζ : IsPrimitiveRoot ζ n) :
      noncomputable def IsPrimitiveRoot.subOnePowerBasis {n : ℕ+} (K : Type u) {L : Type v} [Field K] [CommRing L] [IsDomain L] [Algebra K L] [IsCyclotomicExtension {n} K L] {ζ : L} (hζ : IsPrimitiveRoot ζ n) :

      The PowerBasis given by η - 1.

      Equations
      Instances For
        noncomputable def IsPrimitiveRoot.embeddingsEquivPrimitiveRoots {n : ℕ+} {K : Type u} {L : Type v} [Field K] [CommRing L] [IsDomain L] [Algebra K L] [IsCyclotomicExtension {n} K L] {ζ : L} (hζ : IsPrimitiveRoot ζ n) (C : Type u_1) [CommRing C] [IsDomain C] [Algebra K C] (hirr : Irreducible (Polynomial.cyclotomic (n) K)) :
        (L →ₐ[K] C) { x : C // x primitiveRoots (n) C }

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

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[simp]
          theorem IsPrimitiveRoot.embeddingsEquivPrimitiveRoots_apply_coe {n : ℕ+} {K : Type u} {L : Type v} [Field K] [CommRing L] [IsDomain L] [Algebra K L] [IsCyclotomicExtension {n} K L] {ζ : L} (hζ : IsPrimitiveRoot ζ n) (C : Type u_1) [CommRing C] [IsDomain C] [Algebra K C] (hirr : Irreducible (Polynomial.cyclotomic (n) K)) (φ' : L →ₐ[K] C) :
          ((.embeddingsEquivPrimitiveRoots C hirr) φ') = φ' ζ
          theorem IsCyclotomicExtension.finrank {n : ℕ+} {K : Type u} (L : Type v) [Field K] [CommRing L] [IsDomain L] [Algebra K L] [IsCyclotomicExtension {n} K L] (hirr : Irreducible (Polynomial.cyclotomic (n) K)) :
          FiniteDimensional.finrank K L = (n).totient

          If Irreducible (cyclotomic n K) (in particular for K = ℚ), then the finrank of a cyclotomic extension is n.totient.

          theorem IsPrimitiveRoot.lcm_totient_le_finrank {K : Type u} {L : Type v} [Field K] [CommRing L] [IsDomain L] [Algebra K L] [FiniteDimensional K L] {p : } {q : } {x : L} {y : L} (hx : IsPrimitiveRoot x p) (hy : IsPrimitiveRoot y q) (hirr : Irreducible (Polynomial.cyclotomic (p.lcm q) K)) :
          (p.lcm q).totient FiniteDimensional.finrank K L

          If L contains both a primitive p-th root of unity and q-th root of unity, and Irreducible (cyclotomic (lcm p q) K) (in particular for K = ℚ), then the finrank K L is at least (lcm p q).totient.

          theorem IsPrimitiveRoot.dvd_of_isCyclotomicExtension (n : ℕ+) {K : Type u} [Field K] [NumberField K] [IsCyclotomicExtension {n} K] {ζ : K} {l : } (hζ : IsPrimitiveRoot ζ l) (hl : l 0) :
          l 2 * n

          If a n-th cyclotomic extension of contains a primitive l-th root of unity, then l ∣ 2 * n.

          theorem IsPrimitiveRoot.exists_neg_pow_of_isOfFinOrder {n : ℕ+} {K : Type u} [Field K] [NumberField K] [IsCyclotomicExtension {n} K] (hno : Odd n) {ζ : K} {x : K} (hζ : IsPrimitiveRoot ζ n) (hx : IsOfFinOrder x) :
          ∃ (r : ), x = (-ζ) ^ r

          If x is a root of unity (spelled as IsOfFinOrder x) in an n-th cyclotomic extension of , where n is odd, and ζ is a primitive n-th root of unity, then there exist r such that x = (-ζ)^r.

          theorem IsPrimitiveRoot.exists_pow_or_neg_mul_pow_of_isOfFinOrder {n : ℕ+} {K : Type u} [Field K] [NumberField K] [IsCyclotomicExtension {n} K] (hno : Odd n) {ζ : K} {x : K} (hζ : IsPrimitiveRoot ζ n) (hx : IsOfFinOrder x) :
          r < n, x = ζ ^ r x = -ζ ^ r

          If x is a root of unity (spelled as IsOfFinOrder x) in an n-th cyclotomic extension of , where n is odd, and ζ is a primitive n-th root of unity, then there exists r < n such that x = ζ^r or x = -ζ^r.

          theorem IsPrimitiveRoot.norm_eq_neg_one_pow {K : Type u} {L : Type v} [CommRing L] {ζ : L} [Field K] [Algebra K L] (hζ : IsPrimitiveRoot ζ 2) [IsDomain L] :

          This mathematically trivial result is complementary to norm_eq_one below.

          theorem IsPrimitiveRoot.norm_eq_one {n : ℕ+} {K : Type u} {L : Type v} [CommRing L] {ζ : L} (hζ : IsPrimitiveRoot ζ n) [Field K] [Algebra K L] [IsDomain L] [IsCyclotomicExtension {n} K L] (hn : n 2) (hirr : Irreducible (Polynomial.cyclotomic (n) K)) :
          (Algebra.norm K) ζ = 1

          If Irreducible (cyclotomic n K) (in particular for K = ℚ), the norm of a primitive root is 1 if n ≠ 2.

          theorem IsPrimitiveRoot.norm_eq_one_of_linearly_ordered {n : ℕ+} {L : Type v} [CommRing L] {ζ : L} (hζ : IsPrimitiveRoot ζ n) {K : Type u_1} [LinearOrderedField K] [Algebra K L] (hodd : Odd n) :
          (Algebra.norm K) ζ = 1

          If K is linearly ordered, the norm of a primitive root is 1 if n is odd.

          theorem IsPrimitiveRoot.norm_of_cyclotomic_irreducible {n : ℕ+} (A : Type w) (B : Type z) {K : Type u} {L : Type v} [CommRing A] [CommRing B] [Algebra A B] [IsCyclotomicExtension {n} A B] [CommRing L] {ζ : L} (hζ : IsPrimitiveRoot ζ n) [Field K] [Algebra K L] [IsDomain L] [IsCyclotomicExtension {n} K L] (hirr : Irreducible (Polynomial.cyclotomic (n) K)) :
          (Algebra.norm K) ζ = if n = 2 then -1 else 1
          theorem IsPrimitiveRoot.sub_one_norm_eq_eval_cyclotomic {n : ℕ+} {K : Type u} {L : Type v} [Field L] {ζ : L} (hζ : IsPrimitiveRoot ζ n) [Field K] [Algebra K L] [IsCyclotomicExtension {n} K L] (h : 2 < n) (hirr : Irreducible (Polynomial.cyclotomic (n) K)) :

          If Irreducible (cyclotomic n K) (in particular for K = ℚ), then the norm of ζ - 1 is eval 1 (cyclotomic n ℤ).

          theorem IsPrimitiveRoot.sub_one_norm_isPrimePow {n : ℕ+} {K : Type u} {L : Type v} [Field L] {ζ : L} (hζ : IsPrimitiveRoot ζ n) [Field K] [Algebra K L] (hn : IsPrimePow n) [IsCyclotomicExtension {n} K L] (hirr : Irreducible (Polynomial.cyclotomic (n) K)) (h : n 2) :
          (Algebra.norm K) (ζ - 1) = (n).minFac

          If IsPrimePow (n : ℕ), n ≠ 2 and Irreducible (cyclotomic n K) (in particular for K = ℚ), then the norm of ζ - 1 is (n : ℕ).minFac.

          theorem IsPrimitiveRoot.minpoly_sub_one_eq_cyclotomic_comp {n : ℕ+} {A : Type w} {K : Type u} [CommRing A] [Field K] [Algebra K A] [IsDomain A] {ζ : A} [IsCyclotomicExtension {n} K A] (hζ : IsPrimitiveRoot ζ n) (h : Irreducible (Polynomial.cyclotomic (n) K)) :
          minpoly K (ζ - 1) = (Polynomial.cyclotomic (n) K).comp (Polynomial.X + 1)
          theorem IsPrimitiveRoot.norm_pow_sub_one_of_prime_pow_ne_two {p : ℕ+} {K : Type u} {L : Type v} [Field L] {ζ : L} [Field K] [Algebra K L] {k : } {s : } (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) [hpri : Fact (Nat.Prime p)] [IsCyclotomicExtension {p ^ (k + 1)} K L] (hirr : Irreducible (Polynomial.cyclotomic ((p ^ (k + 1))) K)) (hs : s k) (htwo : p ^ (k - s + 1) 2) :
          (Algebra.norm K) (ζ ^ p ^ s - 1) = p ^ p ^ s

          If Irreducible (cyclotomic (p ^ (k + 1)) K) (in particular for K = ℚ) and p is a prime, then the norm of ζ ^ (p ^ s) - 1 is p ^ (p ^ s) if p ^ (k - s + 1) ≠ 2. See the next lemmas for similar results.

          theorem IsPrimitiveRoot.norm_pow_sub_one_of_prime_ne_two {p : ℕ+} {K : Type u} {L : Type v} [Field L] {ζ : L} [Field K] [Algebra K L] {k : } (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) [hpri : Fact (Nat.Prime p)] [IsCyclotomicExtension {p ^ (k + 1)} K L] (hirr : Irreducible (Polynomial.cyclotomic ((p ^ (k + 1))) K)) {s : } (hs : s k) (hodd : p 2) :
          (Algebra.norm K) (ζ ^ p ^ s - 1) = p ^ p ^ s

          If Irreducible (cyclotomic (p ^ (k + 1)) K) (in particular for K = ℚ) and p is a prime, then the norm of ζ ^ (p ^ s) - 1 is p ^ (p ^ s) if p ≠ 2.

          theorem IsPrimitiveRoot.norm_sub_one_of_prime_ne_two {p : ℕ+} {K : Type u} {L : Type v} [Field L] {ζ : L} [Field K] [Algebra K L] {k : } (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) [hpri : Fact (Nat.Prime p)] [IsCyclotomicExtension {p ^ (k + 1)} K L] (hirr : Irreducible (Polynomial.cyclotomic ((p ^ (k + 1))) K)) (h : p 2) :
          (Algebra.norm K) (ζ - 1) = p

          If Irreducible (cyclotomic (p ^ (k + 1)) K) (in particular for K = ℚ) and p is an odd prime, then the norm of ζ - 1 is p.

          theorem IsPrimitiveRoot.norm_sub_one_of_prime_ne_two' {p : ℕ+} {K : Type u} {L : Type v} [Field L] {ζ : L} [Field K] [Algebra K L] [hpri : Fact (Nat.Prime p)] [hcyc : IsCyclotomicExtension {p} K L] (hζ : IsPrimitiveRoot ζ p) (hirr : Irreducible (Polynomial.cyclotomic (p) K)) (h : p 2) :
          (Algebra.norm K) (ζ - 1) = p

          If Irreducible (cyclotomic p K) (in particular for K = ℚ) and p is an odd prime, then the norm of ζ - 1 is p.

          theorem IsPrimitiveRoot.norm_pow_sub_one_two {K : Type u} {L : Type v} [Field L] {ζ : L} [Field K] [Algebra K L] {k : } (hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))) [IsCyclotomicExtension {2 ^ (k + 1)} K L] (hirr : Irreducible (Polynomial.cyclotomic (2 ^ (k + 1)) K)) :
          (Algebra.norm K) (ζ ^ 2 ^ k - 1) = (-2) ^ 2 ^ k

          If Irreducible (cyclotomic (2 ^ (k + 1)) K) (in particular for K = ℚ), then the norm of ζ ^ (2 ^ k) - 1 is (-2) ^ (2 ^ k).

          theorem IsPrimitiveRoot.norm_sub_one_two {K : Type u} {L : Type v} [Field L] {ζ : L} [Field K] [Algebra K L] {k : } (hζ : IsPrimitiveRoot ζ (2 ^ k)) (hk : 2 k) [H : IsCyclotomicExtension {2 ^ k} K L] (hirr : Irreducible (Polynomial.cyclotomic (2 ^ k) K)) :
          (Algebra.norm K) (ζ - 1) = 2

          If Irreducible (cyclotomic (2 ^ k) K) (in particular for K = ℚ) and k is at least 2, then the norm of ζ - 1 is 2.

          theorem IsPrimitiveRoot.norm_pow_sub_one_eq_prime_pow_of_ne_zero {p : ℕ+} {K : Type u} {L : Type v} [Field L] {ζ : L} [Field K] [Algebra K L] {k : } {s : } (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) [hpri : Fact (Nat.Prime p)] [hcycl : IsCyclotomicExtension {p ^ (k + 1)} K L] (hirr : Irreducible (Polynomial.cyclotomic ((p ^ (k + 1))) K)) (hs : s k) (hk : k 0) :
          (Algebra.norm K) (ζ ^ p ^ s - 1) = p ^ p ^ s

          If Irreducible (cyclotomic (p ^ (k + 1)) K) (in particular for K = ℚ) and p is a prime, then the norm of ζ ^ (p ^ s) - 1 is p ^ (p ^ s) if k ≠ 0 and s ≤ k.

          theorem IsCyclotomicExtension.norm_zeta_eq_one {n : ℕ+} {K : Type u} (L : Type v) [Field K] [Field L] [Algebra K L] [IsCyclotomicExtension {n} K L] (hn : n 2) (hirr : Irreducible (Polynomial.cyclotomic (n) K)) :

          If Irreducible (cyclotomic n K) (in particular for K = ℚ), the norm of zeta n K L is 1 if n is odd.

          theorem IsCyclotomicExtension.norm_zeta_sub_one_of_isPrimePow {n : ℕ+} {K : Type u} (L : Type v) [Field K] [Field L] [Algebra K L] (hn : IsPrimePow n) [IsCyclotomicExtension {n} K L] (hirr : Irreducible (Polynomial.cyclotomic (n) K)) (h : n 2) :
          (Algebra.norm K) (IsCyclotomicExtension.zeta n K L - 1) = (n).minFac

          If IsPrimePow (n : ℕ), n ≠ 2 and Irreducible (cyclotomic n K) (in particular for K = ℚ), then the norm of zeta n K L - 1 is (n : ℕ).minFac.

          theorem IsCyclotomicExtension.norm_zeta_pow_sub_one_of_prime_pow_ne_two {p : ℕ+} {K : Type u} (L : Type v) [Field K] [Field L] [Algebra K L] {k : } [Fact (Nat.Prime p)] [IsCyclotomicExtension {p ^ (k + 1)} K L] (hirr : Irreducible (Polynomial.cyclotomic ((p ^ (k + 1))) K)) {s : } (hs : s k) (htwo : p ^ (k - s + 1) 2) :
          (Algebra.norm K) (IsCyclotomicExtension.zeta (p ^ (k + 1)) K L ^ p ^ s - 1) = p ^ p ^ s

          If Irreducible (cyclotomic (p ^ (k + 1)) K) (in particular for K = ℚ) and p is a prime, then the norm of (zeta (p ^ (k + 1)) K L) ^ (p ^ s) - 1 is p ^ (p ^ s) if p ^ (k - s + 1) ≠ 2.

          theorem IsCyclotomicExtension.norm_zeta_pow_sub_one_of_prime_ne_two {p : ℕ+} {K : Type u} (L : Type v) [Field K] [Field L] [Algebra K L] {k : } [Fact (Nat.Prime p)] [IsCyclotomicExtension {p ^ (k + 1)} K L] (hirr : Irreducible (Polynomial.cyclotomic ((p ^ (k + 1))) K)) (h : p 2) :
          (Algebra.norm K) (IsCyclotomicExtension.zeta (p ^ (k + 1)) K L - 1) = p

          If Irreducible (cyclotomic (p ^ (k + 1)) K) (in particular for K = ℚ) and p is an odd prime, then the norm of zeta (p ^ (k + 1)) K L - 1 is p.

          theorem IsCyclotomicExtension.norm_zeta_sub_one_of_prime_ne_two {p : ℕ+} {K : Type u} (L : Type v) [Field K] [Field L] [Algebra K L] [Fact (Nat.Prime p)] [IsCyclotomicExtension {p} K L] (hirr : Irreducible (Polynomial.cyclotomic (p) K)) (h : p 2) :

          If Irreducible (cyclotomic p K) (in particular for K = ℚ) and p is an odd prime, then the norm of zeta p K L - 1 is p.

          theorem IsCyclotomicExtension.norm_zeta_pow_sub_one_two {K : Type u} (L : Type v) [Field K] [Field L] [Algebra K L] {k : } (hk : 2 k) [IsCyclotomicExtension {2 ^ k} K L] (hirr : Irreducible (Polynomial.cyclotomic (2 ^ k) K)) :

          If Irreducible (cyclotomic (2 ^ k) K) (in particular for K = ℚ) and k is at least 2, then the norm of zeta (2 ^ k) K L - 1 is 2.

          @[deprecated IsPrimitiveRoot.norm_pow_sub_one_of_prime_pow_ne_two]
          theorem IsPrimitiveRoot.pow_sub_one_norm_prime_pow_ne_two {p : ℕ+} {K : Type u} {L : Type v} [Field L] {ζ : L} [Field K] [Algebra K L] {k : } {s : } (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) [hpri : Fact (Nat.Prime p)] [IsCyclotomicExtension {p ^ (k + 1)} K L] (hirr : Irreducible (Polynomial.cyclotomic ((p ^ (k + 1))) K)) (hs : s k) (htwo : p ^ (k - s + 1) 2) :
          (Algebra.norm K) (ζ ^ p ^ s - 1) = p ^ p ^ s

          Alias of IsPrimitiveRoot.norm_pow_sub_one_of_prime_pow_ne_two.


          If Irreducible (cyclotomic (p ^ (k + 1)) K) (in particular for K = ℚ) and p is a prime, then the norm of ζ ^ (p ^ s) - 1 is p ^ (p ^ s) if p ^ (k - s + 1) ≠ 2. See the next lemmas for similar results.

          @[deprecated IsPrimitiveRoot.norm_pow_sub_one_of_prime_ne_two]
          theorem IsPrimitiveRoot.pow_sub_one_norm_prime_ne_two {p : ℕ+} {K : Type u} {L : Type v} [Field L] {ζ : L} [Field K] [Algebra K L] {k : } (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) [hpri : Fact (Nat.Prime p)] [IsCyclotomicExtension {p ^ (k + 1)} K L] (hirr : Irreducible (Polynomial.cyclotomic ((p ^ (k + 1))) K)) {s : } (hs : s k) (hodd : p 2) :
          (Algebra.norm K) (ζ ^ p ^ s - 1) = p ^ p ^ s

          Alias of IsPrimitiveRoot.norm_pow_sub_one_of_prime_ne_two.


          If Irreducible (cyclotomic (p ^ (k + 1)) K) (in particular for K = ℚ) and p is a prime, then the norm of ζ ^ (p ^ s) - 1 is p ^ (p ^ s) if p ≠ 2.

          @[deprecated IsPrimitiveRoot.norm_sub_one_of_prime_ne_two]
          theorem IsPrimitiveRoot.sub_one_norm_prime_ne_two {p : ℕ+} {K : Type u} {L : Type v} [Field L] {ζ : L} [Field K] [Algebra K L] {k : } (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) [hpri : Fact (Nat.Prime p)] [IsCyclotomicExtension {p ^ (k + 1)} K L] (hirr : Irreducible (Polynomial.cyclotomic ((p ^ (k + 1))) K)) (h : p 2) :
          (Algebra.norm K) (ζ - 1) = p

          Alias of IsPrimitiveRoot.norm_sub_one_of_prime_ne_two.


          If Irreducible (cyclotomic (p ^ (k + 1)) K) (in particular for K = ℚ) and p is an odd prime, then the norm of ζ - 1 is p.

          @[deprecated IsPrimitiveRoot.norm_sub_one_of_prime_ne_two']
          theorem IsPrimitiveRoot.sub_one_norm_prime {p : ℕ+} {K : Type u} {L : Type v} [Field L] {ζ : L} [Field K] [Algebra K L] [hpri : Fact (Nat.Prime p)] [hcyc : IsCyclotomicExtension {p} K L] (hζ : IsPrimitiveRoot ζ p) (hirr : Irreducible (Polynomial.cyclotomic (p) K)) (h : p 2) :
          (Algebra.norm K) (ζ - 1) = p

          Alias of IsPrimitiveRoot.norm_sub_one_of_prime_ne_two'.


          If Irreducible (cyclotomic p K) (in particular for K = ℚ) and p is an odd prime, then the norm of ζ - 1 is p.

          @[deprecated IsPrimitiveRoot.norm_pow_sub_one_two]
          theorem IsPrimitiveRoot.pow_sub_one_norm_two {K : Type u} {L : Type v} [Field L] {ζ : L} [Field K] [Algebra K L] {k : } (hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))) [IsCyclotomicExtension {2 ^ (k + 1)} K L] (hirr : Irreducible (Polynomial.cyclotomic (2 ^ (k + 1)) K)) :
          (Algebra.norm K) (ζ ^ 2 ^ k - 1) = (-2) ^ 2 ^ k

          Alias of IsPrimitiveRoot.norm_pow_sub_one_two.


          If Irreducible (cyclotomic (2 ^ (k + 1)) K) (in particular for K = ℚ), then the norm of ζ ^ (2 ^ k) - 1 is (-2) ^ (2 ^ k).

          @[deprecated IsPrimitiveRoot.norm_sub_one_two]
          theorem IsPrimitiveRoot.sub_one_norm_two {K : Type u} {L : Type v} [Field L] {ζ : L} [Field K] [Algebra K L] {k : } (hζ : IsPrimitiveRoot ζ (2 ^ k)) (hk : 2 k) [H : IsCyclotomicExtension {2 ^ k} K L] (hirr : Irreducible (Polynomial.cyclotomic (2 ^ k) K)) :
          (Algebra.norm K) (ζ - 1) = 2

          Alias of IsPrimitiveRoot.norm_sub_one_two.


          If Irreducible (cyclotomic (2 ^ k) K) (in particular for K = ℚ) and k is at least 2, then the norm of ζ - 1 is 2.

          @[deprecated IsPrimitiveRoot.norm_pow_sub_one_eq_prime_pow_of_ne_zero]
          theorem IsPrimitiveRoot.pow_sub_one_norm_prime_pow_of_ne_zero {p : ℕ+} {K : Type u} {L : Type v} [Field L] {ζ : L} [Field K] [Algebra K L] {k : } {s : } (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) [hpri : Fact (Nat.Prime p)] [hcycl : IsCyclotomicExtension {p ^ (k + 1)} K L] (hirr : Irreducible (Polynomial.cyclotomic ((p ^ (k + 1))) K)) (hs : s k) (hk : k 0) :
          (Algebra.norm K) (ζ ^ p ^ s - 1) = p ^ p ^ s

          Alias of IsPrimitiveRoot.norm_pow_sub_one_eq_prime_pow_of_ne_zero.


          If Irreducible (cyclotomic (p ^ (k + 1)) K) (in particular for K = ℚ) and p is a prime, then the norm of ζ ^ (p ^ s) - 1 is p ^ (p ^ s) if k ≠ 0 and s ≤ k.

          @[deprecated IsCyclotomicExtension.norm_zeta_sub_one_of_isPrimePow]
          theorem IsCyclotomicExtension.isPrimePow_norm_zeta_sub_one {n : ℕ+} {K : Type u} (L : Type v) [Field K] [Field L] [Algebra K L] (hn : IsPrimePow n) [IsCyclotomicExtension {n} K L] (hirr : Irreducible (Polynomial.cyclotomic (n) K)) (h : n 2) :
          (Algebra.norm K) (IsCyclotomicExtension.zeta n K L - 1) = (n).minFac

          Alias of IsCyclotomicExtension.norm_zeta_sub_one_of_isPrimePow.


          If IsPrimePow (n : ℕ), n ≠ 2 and Irreducible (cyclotomic n K) (in particular for K = ℚ), then the norm of zeta n K L - 1 is (n : ℕ).minFac.

          @[deprecated IsCyclotomicExtension.norm_zeta_pow_sub_one_of_prime_pow_ne_two]
          theorem IsCyclotomicExtension.prime_ne_two_pow_norm_zeta_pow_sub_one {p : ℕ+} {K : Type u} (L : Type v) [Field K] [Field L] [Algebra K L] {k : } [Fact (Nat.Prime p)] [IsCyclotomicExtension {p ^ (k + 1)} K L] (hirr : Irreducible (Polynomial.cyclotomic ((p ^ (k + 1))) K)) {s : } (hs : s k) (htwo : p ^ (k - s + 1) 2) :
          (Algebra.norm K) (IsCyclotomicExtension.zeta (p ^ (k + 1)) K L ^ p ^ s - 1) = p ^ p ^ s

          Alias of IsCyclotomicExtension.norm_zeta_pow_sub_one_of_prime_pow_ne_two.


          If Irreducible (cyclotomic (p ^ (k + 1)) K) (in particular for K = ℚ) and p is a prime, then the norm of (zeta (p ^ (k + 1)) K L) ^ (p ^ s) - 1 is p ^ (p ^ s) if p ^ (k - s + 1) ≠ 2.

          @[deprecated IsCyclotomicExtension.norm_zeta_pow_sub_one_of_prime_ne_two]
          theorem IsCyclotomicExtension.prime_ne_two_pow_norm_zeta_sub_one {p : ℕ+} {K : Type u} (L : Type v) [Field K] [Field L] [Algebra K L] {k : } [Fact (Nat.Prime p)] [IsCyclotomicExtension {p ^ (k + 1)} K L] (hirr : Irreducible (Polynomial.cyclotomic ((p ^ (k + 1))) K)) (h : p 2) :
          (Algebra.norm K) (IsCyclotomicExtension.zeta (p ^ (k + 1)) K L - 1) = p

          Alias of IsCyclotomicExtension.norm_zeta_pow_sub_one_of_prime_ne_two.


          If Irreducible (cyclotomic (p ^ (k + 1)) K) (in particular for K = ℚ) and p is an odd prime, then the norm of zeta (p ^ (k + 1)) K L - 1 is p.

          @[deprecated IsCyclotomicExtension.norm_zeta_sub_one_of_prime_ne_two]
          theorem IsCyclotomicExtension.prime_ne_two_norm_zeta_sub_one {p : ℕ+} {K : Type u} (L : Type v) [Field K] [Field L] [Algebra K L] [Fact (Nat.Prime p)] [IsCyclotomicExtension {p} K L] (hirr : Irreducible (Polynomial.cyclotomic (p) K)) (h : p 2) :

          Alias of IsCyclotomicExtension.norm_zeta_sub_one_of_prime_ne_two.


          If Irreducible (cyclotomic p K) (in particular for K = ℚ) and p is an odd prime, then the norm of zeta p K L - 1 is p.

          @[deprecated IsCyclotomicExtension.norm_zeta_pow_sub_one_two]
          theorem IsCyclotomicExtension.two_pow_norm_zeta_sub_one {K : Type u} (L : Type v) [Field K] [Field L] [Algebra K L] {k : } (hk : 2 k) [IsCyclotomicExtension {2 ^ k} K L] (hirr : Irreducible (Polynomial.cyclotomic (2 ^ k) K)) :

          Alias of IsCyclotomicExtension.norm_zeta_pow_sub_one_two.


          If Irreducible (cyclotomic (2 ^ k) K) (in particular for K = ℚ) and k is at least 2, then the norm of zeta (2 ^ k) K L - 1 is 2.