theorem
L25 ↗rayClassSubgroup_degree
ClassFieldTheory.rayClassSubgroup_degree
A ray-class subgroup realization has degree equal to the subgroup index.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
noncomputable section
namespace ClassFieldTheory
universe uLean source · statement
theorem rayClassSubgroup_degree
(K : Type u) [Field K] [NumberField K]
(m : RayClassModulus K) (H : Subgroup (RayClassGroup m))
(R : RayClassSubgroupRealization K m H) :
Module.finrank K R.extension = H.index