Module

NarrowRayClassModulus.lean

Nyll.ClassFieldTheory.Definitions.ConductorsAndRayClassFields.NarrowRayClassModulus

1 declaration indexed from sourceView source ↗

Module documentation

Imports2

Imported by9

def

ClassFieldTheory.narrowRayClassModulus

Documentation

The modulus with no finite exponent and positivity at every real place. Its ray class group is the narrow ideal class group.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace ClassFieldTheory
universe u
open scoped Classical in

Lean source · full declaration

def narrowRayClassModulus
    (K : Type u) [Field K] [NumberField K] : RayClassModulus K where
  finitePart := 0
  infinitePart := Finset.univ