A finite abelian extension of K inside Mathlib's chosen separable closure. The inherited order is field inclusion.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace ClassFieldTheory
universe uabbrev FiniteAbelianLocalExtension
(K : Type u) [Field K]The packaged intermediate field is finite-dimensional over the base.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace ClassFieldTheory
universe u
namespace FiniteAbelianLocalExtension
variable {K : Type u} [Field K]instance finiteDimensional (E : FiniteAbelianLocalExtension K) :
FiniteDimensional K E.1The packaged intermediate field is abelian Galois over the base.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace ClassFieldTheory
universe u
namespace FiniteAbelianLocalExtension
variable {K : Type u} [Field K]instance isAbelianGalois (E : FiniteAbelianLocalExtension K) :
IsAbelianGalois K E.1The norm subgroup belonging to a packaged finite abelian extension.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace ClassFieldTheory
universe u
namespace FiniteAbelianLocalExtension
variable {K : Type u} [Field K]def normSubgroup (E : FiniteAbelianLocalExtension K) : Subgroup Kˣ