NYLL
Module

RayClassGroupFinite.lean

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

Module documentation

Finiteness of the ideal-theoretic ray class group

The comparison with the idèlic ray class group identifies this group with a quotient by a finite-index congruence subgroup, so it is finite for every modulus.

Imports3
Imported by1

Declarations

theorem

rayClassGroup_finite

L24 ↗
ClassFieldTheory.rayClassGroup_finite
Documentation

Every ray class group of a number field is finite.

Source context 2 commands

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

namespace ClassFieldTheory
universe u
Lean source · statement
theorem rayClassGroup_finite
    (K : Type u) [Field K] [NumberField K]
    (m : RayClassModulus K) :
    Finite (RayClassGroup m)

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