Module

PublicHigherUnitComparison.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.RayClass.PublicHigherUnitComparison

1 declaration indexed from sourceView source ↗

Module documentation

Comparison of public and idelic higher-unit groups

The reader-facing higher-unit group agrees with the group used in the existing ray-class and idelic implementation. Keep this definitional comparison at the boundary between the two APIs.

Imports2

Imported by2

theorem

rayLocalHigherUnitGroup_eq_rayClass

L27 ↗

ClassFieldTheory.rayLocalHigherUnitGroup_eq_rayClass

Documentation

The public local higher-unit group is the same subgroup as the one used by the existing ray-class implementation.

Source context 4 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory

Lean source · statement

theorem rayLocalHigherUnitGroup_eq_rayClass
    {K : Type} [Field K] [NumberField K]
    (v : HeightOneSpectrum (𝓞 K)) (n : ℕ) :
    rayLocalHigherUnitGroup v n = RayClass.localHigherUnitGroup v n

Module documentation

Comparison of public and idelic higher-unit groups

Declarations

rayLocalHigherUnitGroup_eq_rayClass