Cyclotomic fields

Cyclotomic fields and polynomials, real cyclotomic polynomials, 2cos(2πk/n), cyclotomic units, ramification and inertness in cyclotomic fields.

• Homogenized cyclotomic polynomials
• Infinite cyclotomic products
• Prime divisor bounds for cyclotomic values
• Ramification and inertia in cyclotomic fields
• Real cyclotomic polynomials and 2cos(2πk/n)
• Subfields of cyclotomic fields
• Trace metric on cyclotomic fields

TheoremEmbedding a cyclotomic extension of the rationals#✓fully proved

A cyclotomic extension K of ℚ embeds into any characteristic-zero field L containing a primitive n-th root of unity, sending the distinguished root ζ to it.

theorem IsPrimitiveRoot.exists_ringHom_zeta_eq_of_isCyclotomicExtension
    (n : ℕ) [NeZero n] (K : Type*) [Field K] [Algebra ℚ K]
    [IsCyclotomicExtension {n} ℚ K]
    (L : Type*) [Field L] [CharZero L] (ξ : L) (hξ : IsPrimitiveRoot ξ n) :
    ∃ φ : K →+* L, φ (IsCyclotomicExtension.zeta n ℚ K) = ξ

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.