Theorems · Theorem · number theory

IsPrimitiveRoot.sub_one_norm_eq_eval_cyclotomic

∀ {n : ℕ} [NeZero n] {K : Type u} {L : Type v} [inst : Field L] {ζ : L} [inst_1 : Field K] [inst_2 : Algebra K L],
  IsPrimitiveRoot ζ n →
    ∀ [IsCyclotomicExtension {n} K L],
      2 < n →
        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 ℤ).

Defined in

Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Cited by

3 results in Mathlib

Foundations

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

Assumes

NeZeroFieldFieldAlgebraIsCyclotomicExtension