GlobalClassFieldTheory.GlobalClassFields.closedFiniteIndexClassField_finrank_eq_index
The degree of the selected class field over the original number field is the index of its defining idèle-class subgroup.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped IsMulCommutative NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open Reciprocity
variable {K : Type} [Field K] [NumberField K]Lean source · statement
theorem closedFiniteIndexClassField_finrank_eq_index
(H : Subgroup (IdeleClassGroup K))
(hclosed : IsClosed (H : Set (IdeleClassGroup K)))
[H.FiniteIndex] :
Module.finrank K
(closedFiniteIndexClassField
(K := K) H hclosed) =
H.index