ClassFieldTheory.bigHilbertClassFields_eq
Two big Hilbert class fields inside the same separable closure are equal as intermediate fields.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace ClassFieldTheory
universe uLean source · statement
theorem bigHilbertClassFields_eq
(K : Type u) [Field K] [NumberField K]
(E F : FiniteAbelianExtension K)
(hE : IsBigHilbertClassField E)
(hF : IsBigHilbertClassField F) :
E.1 = F.1