ClassFieldTheory.isSmallHilbertClassField_iff_isBig_of_noReal
Over a number field without real places, the small and big Hilbert class field predicates on a fixed finite abelian extension coincide.
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFieldTheory
universe uLean source · statement
theorem isSmallHilbertClassField_iff_isBig_of_noReal
(K : Type u) [Field K] [NumberField K]
[IsEmpty (RayClassRealPlace K)]
(E : FiniteAbelianExtension K) :
IsSmallHilbertClassField E ↔ IsBigHilbertClassField E