ClassFieldTheory.EmbedsInRayClassField
A finite extension embeds into a ray class field for m. The existential formulation avoids making a global choice of ray class field.
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFieldTheory
universe u vLean source · statement
def EmbedsInRayClassField
(K : Type u) [Field K] [NumberField K]
(L : Type v) [Field L] [NumberField L] [Algebra K L]
(m : RayClassModulus K) : Prop