# mathlibdocumentation

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 #

• is_cyclotomic_extension.rat.is_integral_closure_adjoing_singleton_of_prime_pow: if K is a p ^ k-th cyclotomic extension of ℚ, then (adjoin ℤ {ζ}) is the integral closure of ℤ in K.
• is_cyclotomic_extension.rat.cyclotomic_ring_is_integral_closure_of_prime_pow: the integral closure of ℤ inside cyclotomic_field (p ^ k) ℚ is cyclotomic_ring (p ^ k) ℤ ℚ.
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ζ : (p ^ (k + 1))) (hk : p ^ (k + 1) 2) :
= (-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)] [ K] (hζ : p) (hodd : p 2) :
= (-1) ^ ((p - 1) / 2) * p ^ (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ζ : (p ^ k)) :
= (-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'.

theorem is_cyclotomic_extension.rat.discr_prime_pow_eq_unit_mul_pow' {p : ℕ+} {k : } {K : Type u} [field K] [char_zero K] {ζ : K} [hp : fact (nat.prime p)] [is_cyclotomic_extension {p ^ k} K] (hζ : (p ^ k)) :
∃ (u : ˣ) (n : ), = u * p ^ n

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'.

theorem is_cyclotomic_extension.rat.is_integral_closure_adjoing_singleton_of_prime_pow {p : ℕ+} {k : } {K : Type u} [field K] [char_zero K] {ζ : K} [hp : fact (nat.prime p)] [hcycl : is_cyclotomic_extension {p ^ k} K] (hζ : (p ^ k)) :
K

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

theorem is_cyclotomic_extension.rat.is_integral_closure_adjoing_singleton_of_prime {p : ℕ+} {K : Type u} [field K] [char_zero K] {ζ : K} [hp : fact (nat.prime p)] [hcycl : K] (hζ : p) :
K

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