mathlib documentation

number_theory.cyclotomic.rat

Ring of integers of p ^ n-th cyclotomic fields #

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

Main results #

theorem is_cyclotomic_extension.rat.discr_prime_pow_ne_two' {p : ℕ+} {k : } {K : Type u} [field K] [char_zero K] {ζ : K} [hp : fact (nat.prime p)] [is_cyclotomic_extension {p ^ (k + 1)} K] (hζ : is_primitive_root ζ (p ^ (k + 1))) (hk : p ^ (k + 1) 2) :
algebra.discr ((is_primitive_root.sub_one_power_basis hζ).basis) = (-1) ^ ((p ^ (k + 1)).totient / 2) * p ^ (p ^ k * ((p - 1) * (k + 1) - 1))

The discriminant of the power basis given by ζ - 1.

theorem is_cyclotomic_extension.rat.discr_odd_prime' {p : ℕ+} {K : Type u} [field K] [char_zero K] {ζ : K} [hp : fact (nat.prime p)] [is_cyclotomic_extension {p} K] (hζ : is_primitive_root ζ p) (hodd : p 2) :
theorem is_cyclotomic_extension.rat.discr_prime_pow' {p : ℕ+} {k : } {K : Type u} [field K] [char_zero K] {ζ : K} [hp : fact (nat.prime p)] [is_cyclotomic_extension {p ^ k} K] (hζ : is_primitive_root ζ (p ^ k)) :
algebra.discr ((is_primitive_root.sub_one_power_basis hζ).basis) = (-1) ^ ((p ^ k).totient / 2) * p ^ (p ^ (k - 1) * ((p - 1) * k - 1))

The discriminant of the power basis given by ζ - 1. 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.rat.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 the power basis given by ζ - 1 is u * p ^ n. Often this is enough and less cumbersome to use than is_cyclotomic_extension.rat.discr_prime_pow'.

If K is a p ^ k-th cyclotomic extension of , then (adjoin ℤ {ζ}) is the integral closure of in K.

The integral closure of inside cyclotomic_field (p ^ k) ℚ is cyclotomic_ring (p ^ k) ℤ ℚ.