Theorems · Theorem · number theory

IsPrimitiveRoot.norm_eq_neg_one_pow

∀ {K : Type u} {L : Type v} [inst : CommRing L] {ζ : L} [inst_1 : Field K] [inst_2 : Algebra K L],
  IsPrimitiveRoot ζ 2 → ∀ [IsDomain L], (Algebra.norm K) ζ = (-1) ^ Module.finrank K L

This mathematically trivial result is complementary to norm_eq_one below.

Defined in

Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingFieldAlgebraIsDomain