ClassFieldTheory.IsAbelianConductor.unique
The least modulus characterized by ray-class-field containment is unique.
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFieldTheory
universe u vLean source · statement
theorem IsAbelianConductor.unique
{K : Type u} [Field K] [NumberField K]
{L : Type v} [Field L] [NumberField L] [Algebra K L]
{c d : RayClassModulus K}
(hc : IsAbelianConductor K L c)
(hd : IsAbelianConductor K L d) : c = d