ClassFieldTheory.rayClassSubgroup_quotientEquiv
A ray-class realization identifies its prescribed quotient with its finite abelian Galois group.
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_quotientEquiv
(K : Type u) [Field K] [NumberField K]
(m : RayClassModulus K) (H : Subgroup (RayClassGroup m))
(R : RayClassSubgroupRealization K m H) :
Nonempty ((RayClassGroup m ⧸ H) ≃* (R.extension ≃ₐ[K] R.extension))