Theorems · Theorem · number theory

IsCyclotomicExtension.discr_odd_prime

∀ {p : ℕ} {K : Type u} {L : Type v} {ζ : L} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : IsCyclotomicExtension {p} K L] [hp : Fact (Nat.Prime p)] (hζ : IsPrimitiveRoot ζ p),
  Irreducible (Polynomial.cyclotomic p K) →
    p ≠ 2 → Algebra.discr K ⇑(IsPrimitiveRoot.powerBasis K hζ).basis = (-1) ^ ((p - 1) / 2) * ↑p ^ (p - 2)

If p is an odd prime and IsCyclotomicExtension {p} K L, then discr K (hζ.powerBasis K).basis = (-1) ^ ((p - 1) / 2) * p ^ (p - 2) if Irreducible (cyclotomic p K).

Defined in

Mathlib.NumberTheory.Cyclotomic.Discriminant

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebraIsCyclotomicExtensionFact