← all areas

Namespace IsCyclotomicExtension 12 theorems

Landmarks here: The ring of integers of ℚ(ζ₇) is principal

— 4 · Padic 1 · Rat 7

directly in IsCyclotomicExtension 4

• Galois action on a discrete valuation ring in ℚ(ζₚ) IsCyclotomicExtension.exists_mulSemiringAction_algebraMap_smul_eq_of_isDiscreteValuationRing_of_mem_maximalIdeal 0 below · cited by 1 · depth 21
• Total ramification: p = u varpiᵖ⁻¹ in a DVR containing ζₚ IsCyclotomicExtension.exists_isUnit_natCast_eq_mul_uniformizer_pow_sub_one 1 below · cited by 1 · depth 29
• Ramification of q in ℚ(ζ_{qℓ}): varpi^{q-1}=ε q IsCyclotomicExtension.exists_isUnit_pow_sub_one_eq_mul_natCast_of_isDiscreteValuationRing 0 below · cited by 3 · depth 30
• Discriminant of a cyclotomic power basis divides n^{φ(n)} IsCyclotomicExtension.exists_int_dvd_pow_totient_and_algebraMap_eq_discr_powerBasis 0 below · cited by 1 · depth 35

IsCyclotomicExtension.Padic 1

• Ring of integers of ℚₚ(ζ_{p^k}) is ℤₚ[ζ] IsCyclotomicExtension.Padic.isIntegralClosure_adjoin_singleton_of_prime_pow 0 below · cited by 1 · depth 32

IsCyclotomicExtension.Rat 7

• ℤ[ζ₁₁] is a principal ideal ring IsCyclotomicExtension.Rat.eleven_pid 0 below · cited by 1 · depth 7
• landmark The ring of integers of ℚ(ζ₇) is principal IsCyclotomicExtension.Rat.seven_pid 0 below · cited by 1 · depth 7
• 𝒪_K is a PID for K=ℚ(ζ₁₃) IsCyclotomicExtension.Rat.thirteen_pid 0 below · cited by 1 · depth 7
• DVRs of ℚ(ζₚ) containing p in the maximal ideal IsCyclotomicExtension.Rat.isIntegral_ratLocalizedAt_iff_exists_algebraMap_eq_of_isDiscreteValuationRing 1 below · cited by 3 · depth 22
• Residue field of a DVR in ℚ(ζₚ) above p is generated by ℤ IsCyclotomicExtension.Rat.surjective_algebraMap_int_residueField_of_isDiscreteValuationRing 0 below · cited by 25 · depth 22
• Inertia acts trivially on residue fields of ℚ(ζₚ) IsCyclotomicExtension.Rat.algebraMap_smul_eq_algebraMap_of_isDiscreteValuationRing_of_charP 0 below · cited by 2 · depth 23
• Frobenius fixes the image of a DVR in ℚ(ζₚ) above p IsCyclotomicExtension.Rat.frobenius_comp_algebraMap_eq 1 below · cited by 2 · depth 24