Module

CyclotomicIntermediateField.lean

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.CyclotomicIntermediateField

1 declaration indexed from sourceView source ↗

Module documentation

Cyclotomic intermediate fields inside an algebraic closure

A primitive root in the given closure generates an actual cyclotomic intermediate field. The characteristic only needs to avoid the root order.

Imports3

Mathlib.FieldTheory.IsAlgClosed.Basic
Mathlib.NumberTheory.Cyclotomic.Basic
Mathlib.RingTheory.RootsOfUnity.AlgebraicallyClosed

Imported by4

theorem

exists_cyclotomic_intermediateField

L22 ↗

ValuationTheory.DiscreteValuationField.exists_cyclotomic_intermediateField

Documentation

An algebraic closure contains a cyclotomic intermediate field whenever the root order is nonzero in the base field.

Source context 1 command

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

namespace ValuationTheory.DiscreteValuationField

Lean source · statement

theorem exists_cyclotomic_intermediateField
    (K Ω : Type*) [Field K] [Field Ω] [Algebra K Ω] [IsAlgClosure K Ω]
    (n : ℕ) [NeZero (n : K)] :
    ∃ E : IntermediateField K Ω, IsCyclotomicExtension {n} K E

Module documentation

Cyclotomic intermediate fields inside an algebraic closure

Declarations

exists_cyclotomic_intermediateField