Theorems · Theorem · number theory

IsPrimitiveRoot.sub_one_norm_isPrimePow

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

Defined in: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Cited by: 2 results in Mathlib
Foundations: Depth 215 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: NeZero Field Field Algebra IsCyclotomicExtension

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites31

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement and proof · cited by 62,936
Setstatement · cited by 53,352
Algebrastatement and proof · cited by 11,388
Fieldstatement and proof · cited by 7,404
Polynomialstatement · cited by 5,681
MonoidHomstatement · cited by 3,629
Factproof · cited by 2,726
Nat.Primeproof · cited by 2,059
Polynomial.evalproof · cited by 796
Irreduciblestatement and proof · cited by 496
Int.cast_natCastproof · cited by 393
IsPrimitiveRootstatement and proof · cited by 356

Cited by2

Results whose statement or proof uses this declaration.

IsPrimitiveRoot.norm_pow_sub_one_of_prime_pow_ne_twoproof · cited by 4
IsCyclotomicExtension.norm_zeta_sub_one_of_isPrimePowproof · cited by 0