Module

RayClassFieldDegree.lean

Nyll.ClassFieldTheory.Theorems.ConductorsAndRayClassFields.RayClassFieldDegree

1 declaration indexed from sourceView source ↗

Module documentation

Degree of a ray class field

For any ray class field realization of m, its degree is the cardinality of the ideal-theoretic ray class group. The realization is explicit, so this module does not depend on an implementation-level choice of field.

Imports2

Imported by1

Nyll.ClassFieldTheory.Theorems.ConductorsAndRayClassFields.All

theorem

rayClassField_degree

L27 ↗

ClassFieldTheory.rayClassField_degree

Documentation

The ray class field has degree equal to the ray class number.

Source context 4 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTheory
universe u

Lean source · statement

theorem rayClassField_degree
    (K : Type u) [Field K] [NumberField K]
    (m : RayClassModulus K)
    (R : RayClassFieldRealization K m) :
    Module.finrank K R.extension = Nat.card (RayClassGroup m)

Module documentation

Degree of a ray class field

Declarations

rayClassField_degree