ClassFieldTheory.IsAbelianConductor.mem_infinitePart_iff_realRamified
A real place belongs to the public conductor precisely when it ramifies (complexifies) in the extension.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
noncomputable section
namespace ClassFieldTheoryLean source · statement
theorem IsAbelianConductor.mem_infinitePart_iff_realRamified
{K : Type} [Field K] [NumberField K]
{L : Type} [Field L] [NumberField L]
[Algebra K L] [IsAbelianGalois K L]
{c : RayClassModulus K}
(hc : IsAbelianConductor K L c)
(v : RayClassRealPlace K) :
v ∈ c.infinitePart ↔ ¬ v.1.IsUnramifiedIn L