Module

OrdinaryRayClassModulus.lean

Nyll.ClassFieldTheory.Definitions.ConductorsAndRayClassFields.OrdinaryRayClassModulus

2 declarations indexed from sourceView source ↗

Module documentation

Imports1

Imported by8

def

ClassFieldTheory.ordinaryRayClassModulus

Documentation

The modulus with no finite exponent and no positivity condition. Its ray class group is the ordinary ideal class group.

Source context 2 commands

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

namespace ClassFieldTheory
universe u

Lean source · full declaration

def ordinaryRayClassModulus
    (K : Type u) [Field K] [NumberField K] : RayClassModulus K where
  finitePart := 0
  infinitePart := ∅

theorem

ClassFieldTheory.ordinaryRayClassModulus_le

Documentation

The ordinary class-group modulus is below every ray modulus.

Source context 2 commands

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

namespace ClassFieldTheory
universe u

Lean source · statement

theorem ordinaryRayClassModulus_le
    (K : Type u) [Field K] [NumberField K]
    (m : RayClassModulus K) :
    ordinaryRayClassModulus K ≤ m