# Documentation

Mathlib.NumberTheory.Cyclotomic.Discriminant

# Discriminant of cyclotomic fields #

We compute the discriminant of a p ^ n-th cyclotomic extension.

## Main results #

• IsCyclotomicExtension.discr_odd_prime : if p is an odd prime such that IsCyclotomicExtension {p} K L and Irreducible (cyclotomic p K), then discr K (hζ.powerBasis K).basis = (-1) ^ ((p - 1) / 2) * p ^ (p - 2) for any hζ : IsPrimitiveRoot ζ p.
theorem IsPrimitiveRoot.discr_zeta_eq_discr_zeta_sub_one {n : ℕ+} {K : Type u} [] [] {ζ : K} [ce : ] (hζ : ) :
Algebra.discr ().basis = Algebra.discr ().basis

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.

theorem IsCyclotomicExtension.discr_prime_pow_ne_two {p : ℕ+} {k : } {K : Type u} {L : Type v} {ζ : L} [] [] [Algebra K L] [IsCyclotomicExtension {p ^ (k + 1)} K L] [hp : Fact ()] (hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))) (hirr : Irreducible (Polynomial.cyclotomic (↑(p ^ (k + 1))) K)) (hk : p ^ (k + 1) 2) :
Algebra.discr K ().basis = ↑((-1) ^ (Nat.totient ↑(p ^ (k + 1)) / 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.

theorem IsCyclotomicExtension.discr_prime_pow_ne_two' {p : ℕ+} {k : } {K : Type u} {L : Type v} {ζ : L} [] [] [Algebra K L] [IsCyclotomicExtension {p ^ (k + 1)} K L] [hp : Fact ()] (hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))) (hirr : Irreducible (Polynomial.cyclotomic (↑(p ^ (k + 1))) K)) (hk : p ^ (k + 1) 2) :
Algebra.discr K ().basis = ↑((-1) ^ (p ^ k * (p - 1) / 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 * (p - 1) / 2) * p ^ (p ^ k * ((p - 1) * (k + 1) - 1)) if Irreducible (cyclotomic (p ^ (k + 1)) K)), and p ^ (k + 1) ≠ 2.

theorem IsCyclotomicExtension.discr_prime_pow {p : ℕ+} {k : } {K : Type u} {L : Type v} {ζ : L} [] [] [Algebra K L] [hcycl : IsCyclotomicExtension {p ^ k} K L] [hp : Fact ()] (hζ : IsPrimitiveRoot ζ ↑(p ^ k)) (hirr : Irreducible (Polynomial.cyclotomic (↑(p ^ k)) K)) :
Algebra.discr K ().basis = ↑((-1) ^ (Nat.totient ↑(p ^ k) / 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.

theorem IsCyclotomicExtension.discr_prime_pow_eq_unit_mul_pow {p : ℕ+} {k : } {K : Type u} {L : Type v} {ζ : L} [] [] [Algebra K L] [IsCyclotomicExtension {p ^ k} K L] [hp : Fact ()] (hζ : IsPrimitiveRoot ζ ↑(p ^ k)) (hirr : Irreducible (Polynomial.cyclotomic (↑(p ^ k)) K)) :
u n, Algebra.discr K ().basis = u * ↑(p ^ n)

If p is a prime and IsCyclotomicExtension {p ^ k} K L, then there are u : ℤˣ and n : ℕ such that the discriminant of hζ.powerBasis K is u * p ^ n. Often this is enough and less cumbersome to use than IsCyclotomicExtension.discr_prime_pow.

theorem IsCyclotomicExtension.discr_odd_prime {p : ℕ+} {K : Type u} {L : Type v} {ζ : L} [] [] [Algebra K L] [] [hp : Fact ()] (hζ : ) (hirr : Irreducible ()) (hodd : p 2) :
Algebra.discr K ().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).