Ring of integers of p ^ n-th cyclotomic fields #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. We gather results about cyclotomic extensions of
ℚ. In particular, we compute the ring of integers of ap ^ n-th cyclotomic extension ofℚ.
Main results #
is_cyclotomic_extension.rat.is_integral_closure_adjoin_singleton_of_prime_pow: ifKis ap ^ k-th cyclotomic extension ofℚ, then(adjoin ℤ {ζ})is the integral closure ofℤinK.is_cyclotomic_extension.rat.cyclotomic_ring_is_integral_closure_of_prime_pow: the integral closure ofℤinsidecyclotomic_field (p ^ k) ℚiscyclotomic_ring (p ^ k) ℤ ℚ.
The discriminant of the power basis given by ζ - 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) ℤ ℚ.
The algebra isomorphism adjoin ℤ {ζ} ≃ₐ[ℤ] (𝓞 K), where ζ is a primitive p ^ k-th root of
unity and K is a p ^ k-th cyclotomic extension of ℚ.
Equations
- hζ.adjoin_equiv_ring_of_integers = is_primitive_root._root_.is_primitive_root.adjoin_equiv_ring_of_integers._match_1 _
The integral power_basis of 𝓞 K given by a primitive root of unity, where K is a p ^ k
cyclotomic extension of ℚ.
Equations
The algebra isomorphism adjoin ℤ {ζ} ≃ₐ[ℤ] (𝓞 K), where ζ is a primitive p-th root of
unity and K is a p-th cyclotomic extension of ℚ.
Equations
The ring of integers of a p-th cyclotomic extension of ℚ is a cyclotomic extension.
The integral power_basis of 𝓞 K given by a primitive root of unity, where K is a p-th
cyclotomic extension of ℚ.
Equations
The integral power_basis of 𝓞 K given by ζ - 1, where K is a p ^ k cyclotomic
extension of ℚ.
Equations
The integral power_basis of 𝓞 K given by ζ - 1, where K is a p-th cyclotomic
extension of ℚ.