All.lean

General finite-level Lubin--Tate theory

Public aggregate for the characteristic-independent standard division polynomials, primitive torsion fields, analytic formal-module action, explicit finite Galois parameterization, integral-closure valuation, ramification filtrations and their Herbrand formula, level-field tower, and the norm of a primitive uniformizer. It also exports stability of a standard level under a principal-unit change of its defining uniformizer.