Discriminant of cyclotomic fields #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. We compute the discriminant of a
p ^ n-th cyclotomic extension.
Main results #
is_cyclotomic_extension.discr_odd_prime: ifpis an odd prime such thatis_cyclotomic_extension {p} K Landirreducible (cyclotomic p K), thendiscr K (hζ.power_basis K).basis = (-1) ^ ((p - 1) / 2) * p ^ (p - 2)for anyhζ : is_primitive_root ζ p.
The discriminant of the power basis given by a primitive root of unity ζ is the same as the
discriminant of the power basis given by ζ - 1.
If p is a prime and is_cyclotomic_extension {p ^ (k + 1)} K L, then the discriminant of
hζ.power_basis 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.
If p is a prime and is_cyclotomic_extension {p ^ (k + 1)} K L, then the discriminant of
hζ.power_basis K is (-1) ^ (p ^ k * (p - 1) / 2) * p ^ (p ^ k * ((p - 1) * (k + 1) - 1))
if irreducible (cyclotomic (p ^ (k + 1)) K)), and p ^ (k + 1) ≠ 2.
If p is a prime and is_cyclotomic_extension {p ^ k} K L, then the discriminant of
hζ.power_basis 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 is_cyclotomic_extension.discr_prime_pow_eq_unit_mul_pow.
If p is a prime and is_cyclotomic_extension {p ^ k} K L, then there are u : ℤˣ and
n : ℕ such that the discriminant of hζ.power_basis K is u * p ^ n. Often this is enough and
less cumbersome to use than is_cyclotomic_extension.discr_prime_pow.
If p is an odd prime and is_cyclotomic_extension {p} K L, then
discr K (hζ.power_basis K).basis = (-1) ^ ((p - 1) / 2) * p ^ (p - 2) if
irreducible (cyclotomic p K).