Theorems · Theorem · number theory

IsCyclotomicExtension.discr_prime_pow

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

If p is a prime and IsCyclotomicExtension {p ^ k} K L, then the discriminant of hζ.powerBasis K is (-1) ^ ((p ^ k).totient / 2) * p ^ (p ^ (k - 1) * ((p - 1) * k - 1)) if Irreducible (cyclotomic (p ^ k) K)). Beware that in the cases p ^ k = 1 and p ^ k = 2 the formula uses 1 / 2 = 0 and 0 - 1 = 0. It is useful only to have a uniform result. See also IsCyclotomicExtension.discr_prime_pow_eq_unit_mul_pow.

Defined in

Mathlib.NumberTheory.Cyclotomic.Discriminant

Cited by

3 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebraIsCyclotomicExtensionFact