Module

BigHilbertClassFieldDegree.lean

Nyll.ClassFieldTheory.Theorems.FrobeniusAndHilbertClassFields.BigHilbertClassFieldDegree

1 declaration indexed from sourceView source ↗

Module documentation

Degree of the big Hilbert class field

The degree of any extension satisfying the intrinsic big-Hilbert-class-field property is the order of the narrow ray class group. The latter is the ray class group for the modulus containing every real place and no finite prime.

Imports6

Imported by1

Nyll.ClassFieldTheory.Theorems.FrobeniusAndHilbertClassFields.All

theorem

bigHilbertClassField_degree_eq_narrowClassGroup_card

L29 ↗

ClassFieldTheory.bigHilbertClassField_degree_eq_narrowClassGroup_card

Documentation

The big Hilbert class field has degree equal to the narrow class number.

Source context 3 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTheory

Lean source · statement

theorem bigHilbertClassField_degree_eq_narrowClassGroup_card
    (K : Type) [Field K] [NumberField K]
    (E : FiniteAbelianExtension K) (hE : IsBigHilbertClassField E) :
    Module.finrank K E =
      Nat.card (RayClassGroup (narrowRayClassModulus K))

Module documentation

Degree of the big Hilbert class field

Declarations

bigHilbertClassField_degree_eq_narrowClassGroup_card