NYLL
Module

All.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.LubinTateApplication.All
0 declarations indexed from sourceView source ↗

Module documentation

Lubin--Tate application to local class field theory

This is the dependency boundary between reusable Lubin--Tate theory and its local-class-field-theory application. Finite local reciprocity identifies the exact norm subgroup both for the canonical characteristic-independent standard levels and for the transported Laurent-series model. The lower LubinTate public root and all modules below it remain independent of LocalClassFieldTheory.

Imports20
Imported by1

Declarations

This module has no indexed declarations. Its imports and full source are available here.

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