Theorems · Theorem · number theory

IsCyclotomicExtension.discr_prime_pow_ne_two

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

If p is a prime and IsCyclotomicExtension {p ^ (k + 1)} K L, then the discriminant of hζ.powerBasis K is (-1) ^ ((p ^ (k + 1).totient) / 2) * p ^ (p ^ k * ((p - 1) * (k + 1) - 1)) if Irreducible (cyclotomic (p ^ (k + 1)) K)), and p ^ (k + 1) ≠ 2.

Defined in

Mathlib.NumberTheory.Cyclotomic.Discriminant

Cited by

4 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebraIsCyclotomicExtensionFact