ClassFieldTheory.ordinaryRayRealization_isSmallHilbertClassField
Every realization of the ordinary ray class group is a small 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 ordinaryRayRealization_isSmallHilbertClassField
(K : Type) [Field K] [NumberField K]
(R : RayClassFieldRealization K (ordinaryRayClassModulus K)) :
IsSmallHilbertClassField R.extension