ClassFieldTheory.ordinaryRayClassModulus_eq_narrow_of_noReal
If the base number field has no real places, the ordinary and narrow class-group moduli coincide.
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFieldTheory
universe uLean source · statement
theorem ordinaryRayClassModulus_eq_narrow_of_noReal
(K : Type u) [Field K] [NumberField K]
[IsEmpty (RayClassRealPlace K)] :
ordinaryRayClassModulus K = narrowRayClassModulus K