Theorems · Theorem · number theory

IsCyclotomicExtension.Rat.discr_prime_pow

∀ (p k : ℕ) (K : Type u) [inst : Field K] [hp : Fact (Nat.Prime p)] [inst_1 : CharZero K]
  [inst_2 : IsCyclotomicExtension {p ^ k} ℚ K],
  NumberField.discr K = (-1) ^ ((p ^ k).totient / 2) * ↑p ^ (p ^ (k - 1) * ((p - 1) * k - 1))

We compute the absolute discriminant of a p ^ k-th cyclotomic field. Beware that in the cases p ^ k = 1 and p ^ k = 2 the formula uses 1 / 2 = 0 and 0 - 1 = 0. See also the results below.

Defined in

Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

FieldFactCharZeroIsCyclotomicExtension