All.lean

Finite local existence theorem

The ordinary norm-subgroup assignment is an order embedding into the opposite poset of native open finite-index subgroups. Kummer theory in characteristic zero and transported Lubin--Tate levels in positive characteristic prove the existing characteristic-specific order isomorphisms. The canonical standard Lubin--Tate construction now also provides a characteristic-independent finite abelian factor with its exact norm subgroup.