NYLL
Module

CyclotomicField.lean

Nyll.GaloisCohomology.Kummer.Concrete.CyclotomicField
2 declarations indexed from sourceView source ↗

Module documentation

Concrete cyclotomic fields

This file records two structural facts about the concrete cyclotomic-field model: it admits a primitive generator of the defining order, and divisibility of orders induces an algebra homomorphism between the corresponding fields.

Imports2
  • Mathlib.FieldTheory.Galois.Abelian
  • Mathlib.NumberTheory.Cyclotomic.Basic
Imported by2

Declarations

theorem

exists_primitiveRoot_adjoin_eq_top_cyclotomicField

L24 ↗
KummerTheory.exists_primitiveRoot_adjoin_eq_top_cyclotomicField
Documentation

A concrete cyclotomic field has a primitive generator of its defining order.

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace KummerTheory
Lean source · statement
theorem exists_primitiveRoot_adjoin_eq_top_cyclotomicField
    (K : Type) [Field K] [CharZero K] (m : ℕ) (hm : 0 < m) :
    ∃ ζ : CyclotomicField m K,
      IsPrimitiveRoot ζ m ∧ Algebra.adjoin K ({ζ} : Set _) = ⊤
theorem

nonempty_algHom_cyclotomicField_of_dvd

L37 ↗
KummerTheory.nonempty_algHom_cyclotomicField_of_dvd
Documentation

If a divides b, the concrete cyclotomic field of order a embeds in the concrete cyclotomic field of order b.

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace KummerTheory
Lean source · statement
theorem nonempty_algHom_cyclotomicField_of_dvd
    (K : Type) [Field K] [CharZero K]
    (a b : ℕ) (ha : 0 < a) (hb : 0 < b) (hab : a ∣ b) :
    Nonempty (CyclotomicField a K →ₐ[K] CyclotomicField b K)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.