ClassFieldTheory.smallHilbertClassField_degree_eq_classNumber
The small Hilbert class field has degree equal to the class number.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
noncomputable section
namespace ClassFieldTheoryLean source · statement
theorem smallHilbertClassField_degree_eq_classNumber
(K : Type) [Field K] [NumberField K]
(E : FiniteAbelianExtension K) (hE : IsSmallHilbertClassField E) :
Module.finrank K E = NumberField.classNumber K