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

• 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.pow_sub_one_norm_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.sub_one_norm_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.

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

• IsCyclotomicExtension.zeta n A B = Exists.choose ⋯

@[simp]

theorem IsCyclotomicExtension.zeta_spec (n : ℕ+) (A : Type w) (B : Type z) [CommRing A] [CommRing B] [Algebra A B] [IsCyclotomicExtension {n} A B] : IsPrimitiveRoot (IsCyclotomicExtension.zeta n A B) ↑n

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

theorem IsCyclotomicExtension.aeval_zeta (n : ℕ+) (A : Type w) (B : Type z) [CommRing A] [CommRing B] [Algebra A B] [IsCyclotomicExtension {n} A B] [IsDomain B] [NeZero ↑↑n] : (Polynomial.aeval (IsCyclotomicExtension.zeta n A B)) (Polynomial.cyclotomic (↑n) A) = 0

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] : Polynomial.IsRoot (Polynomial.cyclotomic (↑n) B) (IsCyclotomicExtension.zeta n A B)

theorem IsCyclotomicExtension.zeta_pow (n : ℕ+) (A : Type w) (B : Type z) [CommRing A] [CommRing B] [Algebra A B] [IsCyclotomicExtension {n} A B] : IsCyclotomicExtension.zeta n A B ^ ↑n = 1

@[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 hζ).dim = Polynomial.natDegree (minpoly K ζ)

@[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) : (IsPrimitiveRoot.powerBasis K hζ).gen = ζ

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) : PowerBasis K L

The PowerBasis given by a primitive root η.

Equations

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

theorem IsPrimitiveRoot.powerBasis_gen_mem_adjoin_zeta_sub_one {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}

@[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 hζ).dim = Polynomial.natDegree (minpoly K (ζ - 1))

@[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) : (IsPrimitiveRoot.subOnePowerBasis K hζ).gen = ζ - 1

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) : PowerBasis K L

The PowerBasis given by η - 1.

Equations

• IsPrimitiveRoot.subOnePowerBasis K hζ = PowerBasis.ofGenMemAdjoin (IsPrimitiveRoot.powerBasis K hζ) ⋯ ⋯

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.

@[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) : ↑((IsPrimitiveRoot.embeddingsEquivPrimitiveRoots hζ 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 = Nat.totient ↑n

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 (Nat.lcm p q) K)) : Nat.totient (Nat.lcm p q) ≤ 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] : (Algebra.norm K) ζ = (-1) ^ FiniteDimensional.finrank K 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)) : (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 ℤ).

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) = ↑(Nat.minFac ↑n)

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.comp (Polynomial.cyclotomic (↑n) K) (Polynomial.X + 1)

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

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

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

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

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

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

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

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

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

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)) : (Algebra.norm K) (IsCyclotomicExtension.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.

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) = ↑(Nat.minFac ↑n)

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

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

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.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) : (Algebra.norm K) (IsCyclotomicExtension.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.

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)) : (Algebra.norm K) (IsCyclotomicExtension.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.