ClassFieldTheory.isUpperRamificationJump_int
Every actual upper ramification jump of a finite Abelian local extension is an integer, including the possible endpoint -1.
Source context 1 command
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFieldTheoryLean source · statement
theorem isUpperRamificationJump_int
(K L : Type) [Field K] [Field L] [Algebra K L]
[FiniteDimensional K L] [IsAbelianGalois K L]
[ValuativeRel K] [TopologicalSpace K]
[IsNonarchimedeanLocalField K]
[ValuativeRel L] [TopologicalSpace L]
[IsNonarchimedeanLocalField L]
[Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
{t : ℝ} (ht : IsUpperRamificationJump K L t) :
∃ z : ℤ, t = (z : ℝ)