Theorems · Theorem · number theory

IsPrimitiveRoot.norm_toInteger_pow_sub_one_of_two

∀ {k : ℕ} {K : Type u} [inst : Field K] {ζ : K} [inst_1 : CharZero K] [IsCyclotomicExtension {2 ^ (k + 1)} ℚ K]
  (hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))), (Algebra.norm ℤ) (hζ.toInteger ^ 2 ^ k - 1) = (-2) ^ 2 ^ k

The norm, relative to ℤ, of ζ ^ 2 ^ k - 1 in a 2 ^ (k + 1)-th cyclotomic extension of ℚ is (-2) ^ 2 ^ k.

Defined in

Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldCharZeroIsCyclotomicExtension