NYLL
Module

FiniteAbelianExtension.lean

Nyll.ClassFieldTheory.Definitions.GlobalClassFieldTheory.FiniteAbelianExtension
7 declarations indexed from sourceView source ↗

Module documentation

Finite abelian extensions of number fields

This module packages finite abelian extensions inside Mathlib's chosen separable closure. It contains no class-field-theory implementation.

Imports3
  • Mathlib.FieldTheory.Galois.Abelian
  • Mathlib.FieldTheory.IsSepClosed
  • Mathlib.NumberTheory.NumberField.Basic
Imported by14

Declarations

abbrev

FiniteAbelianExtension

L28 ↗
ClassFieldTheory.FiniteAbelianExtension
Documentation

A finite abelian extension of a number field inside Mathlib's chosen separable closure. The inherited order is inclusion of intermediate fields.

Source context 3 commands

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

noncomputable section
namespace ClassFieldTheory
universe u
Lean source · statement
abbrev FiniteAbelianExtension
    (K : Type u) [Field K] [NumberField K]
instance

(anonymous instance)

L35 ↗
Source context 4 commands

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

noncomputable section
namespace ClassFieldTheory
universe u
namespace FiniteAbelianExtension
Lean source · full declaration
instance {K : Type u} [Field K] [NumberField K] :
    CoeSort (FiniteAbelianExtension K) (Type u) where
  coe E := E.1
instance

(anonymous instance)

L39 ↗
Source context 4 commands

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

noncomputable section
namespace ClassFieldTheory
universe u
namespace FiniteAbelianExtension
Lean source · statement
instance {K : Type u} [Field K] [NumberField K]
    (E : FiniteAbelianExtension K) : Field E
instance

(anonymous instance)

L43 ↗
Source context 4 commands

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

noncomputable section
namespace ClassFieldTheory
universe u
namespace FiniteAbelianExtension
Lean source · statement
instance {K : Type u} [Field K] [NumberField K]
    (E : FiniteAbelianExtension K) : FiniteDimensional K E
instance

(anonymous instance)

L47 ↗
Source context 4 commands

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

noncomputable section
namespace ClassFieldTheory
universe u
namespace FiniteAbelianExtension
Lean source · statement
instance {K : Type u} [Field K] [NumberField K]
    (E : FiniteAbelianExtension K) : Algebra K E
instance

(anonymous instance)

L51 ↗
Source context 4 commands

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

noncomputable section
namespace ClassFieldTheory
universe u
namespace FiniteAbelianExtension
Lean source · statement
instance {K : Type u} [Field K] [NumberField K]
    (E : FiniteAbelianExtension K) : NumberField E
instance

(anonymous instance)

L55 ↗
Source context 4 commands

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

noncomputable section
namespace ClassFieldTheory
universe u
namespace FiniteAbelianExtension
Lean source · statement
instance {K : Type u} [Field K] [NumberField K]
    (E : FiniteAbelianExtension K) : IsAbelianGalois K E

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