NYLL
Module

RayClassFieldReciprocity.lean

Nyll.ClassFieldTheory.Theorems.ConductorsAndRayClassFields.RayClassFieldReciprocity
1 declaration indexed from sourceView source ↗

Module documentation

Ray class reciprocity

For a modulus m, there exists a finite abelian extension whose Galois group is the ideal-theoretic ray class group modulo m, compatibly with finite global reciprocity. No global choice of ray class field is exposed.

Imports2
Imported by2

Declarations

theorem

rayClassField_reciprocity

L25 ↗
ClassFieldTheory.rayClassField_reciprocity
Documentation

A ray class field realization exists for every modulus.

Source context 3 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTheory
Lean source · statement
theorem rayClassField_reciprocity
    (K : Type) [Field K] [NumberField K]
    (m : RayClassModulus K) :
    Nonempty (RayClassFieldRealization K m)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.