ClassFieldTheory.narrowRayRealization_isBigHilbertClassField
Every realization of the narrow ray class group is a big Hilbert class field, including its maximality property.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
noncomputable section
namespace ClassFieldTheory
open NumberField IsDedekindDomainLean source · statement
theorem narrowRayRealization_isBigHilbertClassField
(K : Type) [Field K] [NumberField K]
(R : RayClassFieldRealization K (narrowRayClassModulus K)) :
IsBigHilbertClassField R.extension