ClassFieldTheory.IsBigHilbertClassField
A big Hilbert class field is a finite-prime-unramified finite abelian extension containing every finite abelian extension unramified at the finite places. Ramification at real places is allowed.
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFieldTheory
universe uLean source · statement
def IsBigHilbertClassField
{K : Type u} [Field K] [NumberField K]
(E : FiniteAbelianExtension K) : Prop