# Primitive roots in cyclotomic fields #

If `IsCyclotomicExtension {n} A B`, we define an element `zeta n A B : B` that is a primitive `n`th-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 #

- `IsCyclotomicExtension.zeta n A B`: if `IsCyclotomicExtension {n} A B`, than `zeta n A B` is a primitive `n`-th root of unity in `B`.
- `IsPrimitiveRoot.powerBasis`: if `K` and `L` are fields such that `IsCyclotomicExtension {n} K L`, then `IsPrimitiveRoot.powerBasis` gives a `K`-power basis for `L` given a primitive root `ζ`.
- `IsPrimitiveRoot.embeddingsEquivPrimitiveRoots`: the equivalence between `L →ₐ[K] A` and `primitiveRoots n A` given by the choice of `ζ`.

## Main results #

- `IsCyclotomicExtension.zeta_spec`: `zeta n A B` is a primitive `n`-th root of unity.
- `IsCyclotomicExtension.finrank`: if `Irreducible (cyclotomic n K)` (in particular for `K = ℚ`), then the `finrank` of a cyclotomic extension is `n.totient`.
- `IsPrimitiveRoot.norm_eq_one`: if `Irreducible (cyclotomic n K)` (in particular for `K = ℚ`), the norm of a primitive root is `1` if `n ≠ 2`.
- `IsPrimitiveRoot.sub_one_norm_eq_eval_cyclotomic`: if `Irreducible (cyclotomic n K)` (in particular for `K = ℚ`), then the norm of `ζ - 1` is `eval 1 (cyclotomic n ℤ)`, for a primitive root `ζ`. We also prove the analogous of this result for `zeta`.
- `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)` `p ^ (k - s + 1) ≠ 2`. See the following lemmas for similar results. We also prove the analogous of this result for `zeta`.
- `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`. We also prove the analogous of this result for `zeta`.
- `IsPrimitiveRoot.embeddingsEquivPrimitiveRoots`: the equivalence between `L →ₐ[K] A` and `primitiveRoots n A` given by the choice of `ζ`.

## 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`.

source
noncomputable def IsCyclotomicExtension.zeta (n : ℕ) [NeZero 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

- IsCyclotomicExtension.zeta n A B = ⋯.choose

Instances For

source
@[simp]
theorem IsCyclotomicExtension.zeta_spec (n : ℕ) [NeZero n] (A : Type w) (B : Type z) [CommRing A] [CommRing B] [Algebra A B] [IsCyclotomicExtension {n} A B] :
IsPrimitiveRoot (zeta n A B) n

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

source
theorem IsCyclotomicExtension.aeval_zeta (n : ℕ) [NeZero n] (A : Type w) (B : Type z) [CommRing A] [CommRing B] [Algebra A B] [IsCyclotomicExtension {n} A B] [IsDomain B] [NeZero ↑n] :
(Polynomial.aeval (zeta n A B)) (Polynomial.cyclotomic n A) = 0
source
theorem IsCyclotomicExtension.zeta_isRoot (n : ℕ) [NeZero n] (A : Type w) (B : Type z) [CommRing A] [CommRing B] [Algebra A B] [IsCyclotomicExtension {n} A B] [IsDomain B] [NeZero ↑n] :
(Polynomial.cyclotomic n B).IsRoot (zeta n A B)
source
theorem IsCyclotomicExtension.zeta_pow (n : ℕ) [NeZero n] (A : Type w) (B : Type z) [CommRing A] [CommRing B] [Algebra A B] [IsCyclotomicExtension {n} A B] :
zeta n A B ^ n = 1
source
noncomputable def IsPrimitiveRoot.powerBasis {n : ℕ} [NeZero n] (K : Type u) {L : Type v} [Field K] [CommRing L] [IsDomain L] [Algebra K L] [IsCyclotomicExtension {n} K L] {ζ : L} (hζ : IsPrimitiveRoot ζ n) :
PowerBasis K L

The `PowerBasis` given by a primitive root `η`.

Equations

- IsPrimitiveRoot.powerBasis K hζ = (Algebra.adjoin.powerBasis ⋯).map (((Algebra.adjoin K {ζ}).equivOfEq ⊤ ⋯).trans Subalgebra.topEquiv)

Instances For

source
@[simp]
theorem IsPrimitiveRoot.powerBasis_gen {n : ℕ} [NeZero 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 hζ).gen = ζ
source
@[simp]
theorem IsPrimitiveRoot.powerBasis_dim {n : ℕ} [NeZero 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 hζ).dim = (minpoly K ζ).natDegree
source
theorem IsPrimitiveRoot.powerBasis_gen_mem_adjoin_zeta_sub_one {n : ℕ} [NeZero 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 hζ).gen ∈ Algebra.adjoin K {ζ - 1}
source
noncomputable def IsPrimitiveRoot.subOnePowerBasis {n : ℕ} [NeZero n] (K : Type u) {L : Type v} [Field K] [CommRing L] [IsDomain L] [Algebra K L] [IsCyclotomicExtension {n} K L] {ζ : L} (hζ : IsPrimitiveRoot ζ n) :
PowerBasis K L

The `PowerBasis` given by `η - 1`.

Equations

- IsPrimitiveRoot.subOnePowerBasis K hζ = PowerBasis.ofAdjoinEqTop ⋯ ⋯

Instances For

source
@[simp]
theorem IsPrimitiveRoot.subOnePowerBasis_dim {n : ℕ} [NeZero n] (K : Type u) {L : Type v} [Field K] [CommRing L] [IsDomain L] [Algebra K L] [IsCyclotomicExtension {n} K L] {ζ : L} (hζ : IsPrimitiveRoot ζ n) :
(subOnePowerBasis K hζ).dim = (minpoly K (ζ - 1)).natDegree
source
@[simp]
theorem IsPrimitiveRoot.subOnePowerBasis_gen {n : ℕ} [NeZero n] (K : Type u) {L : Type v} [Field K] [CommRing L] [IsDomain L] [Algebra K L] [IsCyclotomicExtension {n} K L] {ζ : L} (hζ : IsPrimitiveRoot ζ n) :
(subOnePowerBasis K hζ).gen = ζ - 1
source
noncomputable def IsPrimitiveRoot.embeddingsEquivPrimitiveRoots {n : ℕ} [NeZero 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) ≃ ↥(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

source
@[simp]
theorem IsPrimitiveRoot.embeddingsEquivPrimitiveRoots_apply_coe {n : ℕ} [NeZero 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) :
↑((hζ.embeddingsEquivPrimitiveRoots C hirr) φ') = φ' ζ
source
theorem IsCyclotomicExtension.finrank {n : ℕ} [NeZero 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)) :
Module.finrank K L = n.totient

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

source
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 y : L} (hx : IsPrimitiveRoot x p) (hy : IsPrimitiveRoot y q) (hirr : Irreducible (Polynomial.cyclotomic (p.lcm q) K)) :
(p.lcm q).totient ≤ Module.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`.

source
theorem IsPrimitiveRoot.dvd_of_isCyclotomicExtension (n : ℕ) [NeZero 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`.

source
theorem IsPrimitiveRoot.exists_neg_pow_of_isOfFinOrder {n : ℕ} [NeZero n] {K : Type u} [Field K] [NumberField K] [IsCyclotomicExtension {n} ℚ K] (hno : Odd n) {ζ 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`.

source
theorem IsPrimitiveRoot.exists_pow_or_neg_mul_pow_of_isOfFinOrder {n : ℕ} [NeZero n] {K : Type u} [Field K] [NumberField K] [IsCyclotomicExtension {n} ℚ K] (hno : Odd n) {ζ 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`.

source
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] :
(Algebra.norm K) ζ = (-1) ^ Module.finrank K L

This mathematically trivial result is complementary to `norm_eq_one` below.

source
theorem IsPrimitiveRoot.norm_eq_one {n : ℕ} [NeZero n] {K : Type u} {L : Type v} [CommRing L] {ζ : L} [Field K] [Algebra K L] (hζ : IsPrimitiveRoot ζ n) [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`.

source
theorem IsPrimitiveRoot.norm_eq_one_of_linearly_ordered {n : ℕ} {L : Type v} [CommRing L] {ζ : L} (hζ : IsPrimitiveRoot ζ n) {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing 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.

source
theorem IsPrimitiveRoot.norm_of_cyclotomic_irreducible {n : ℕ} [NeZero n] {K : Type u} {L : Type v} [CommRing L] {ζ : L} [Field K] [Algebra K L] (hζ : IsPrimitiveRoot ζ n) [IsDomain L] [IsCyclotomicExtension {n} K L] (hirr : Irreducible (Polynomial.cyclotomic n K)) :
(Algebra.norm K) ζ = if n = 2 then -1 else 1
source
theorem IsPrimitiveRoot.sub_one_norm_eq_eval_cyclotomic {n : ℕ} [NeZero n] {K : Type u} {L : Type v} [Field L] {ζ : L} [Field K] [Algebra K L] (hζ : IsPrimitiveRoot ζ n) [IsCyclotomicExtension {n} K L] (h : 2 < n) (hirr : Irreducible (Polynomial.cyclotomic n K)) :
(Algebra.norm K) (ζ - 1) = ↑(Polynomial.eval 1 (Polynomial.cyclotomic n ℤ))

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

source
theorem IsPrimitiveRoot.sub_one_norm_isPrimePow {n : ℕ} [NeZero n] {K : Type u} {L : Type v} [Field L] {ζ : L} [Field K] [Algebra K L] (hζ : IsPrimitiveRoot ζ n) (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`.

source
theorem IsPrimitiveRoot.minpoly_sub_one_eq_cyclotomic_comp {n : ℕ} [NeZero 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)
source
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.

source
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`.

source
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`.

source
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`.

source
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)`.

source
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`.

source
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`.

source
theorem IsCyclotomicExtension.norm_zeta_eq_one {n : ℕ} [NeZero 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)) :
(Algebra.norm K) (zeta n K L) = 1

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

source
theorem IsCyclotomicExtension.norm_zeta_sub_one_of_isPrimePow {n : ℕ} [NeZero 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) (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`.

source
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) (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`.

source
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) (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`.

source
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) :
(Algebra.norm K) (zeta p K L - 1) = ↑p

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`.

source
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)) :
(Algebra.norm K) (zeta (2 ^ k) K L - 1) = 2

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`.