ClassFieldTheory.IsAbelianConductor
A modulus is the conductor of a finite abelian extension when it is exactly the least modulus whose ray class field contains the extension.
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFieldTheory
universe u vLean source · statement
def IsAbelianConductor
(K : Type u) [Field K] [NumberField K]
(L : Type v) [Field L] [NumberField L] [Algebra K L]
(c : RayClassModulus K) : Prop