Module

NormLimitationStatement.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.IdealClassFieldTheory.NormLimitationStatement

1 declaration indexed from sourceView source ↗

Module documentation

Statement boundary for ideal norm limitation

This leaf packages the ideal norm-limitation equality behind a named proposition. Keeping the expanded normal-closure expression out of later declaration signatures avoids repeatedly normalizing the full finite tower.

Imports2

Imported by2

def

idealNormSubgroupMaximalAbelianStatement

L33 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.idealNormSubgroupMaximalAbelianStatement

Documentation

The proposition asserting ideal norm limitation for one defining modulus.

Source context 5 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
variable
    (K L : Type)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]

Lean source · statement

def idealNormSubgroupMaximalAbelianStatement
    (m : RayClass.Modulus K)
    (_hm :
      RayClass.Modulus.congruenceSubgroup m ≤
        (_root_.ideleClassNorm K L).range) : Prop

Module documentation

Statement boundary for ideal norm limitation

Declarations

idealNormSubgroupMaximalAbelianStatement