ClassFieldTheory.upperRamificationGroup_eventually_bot
The canonical upper ramification groups of a finite Abelian local extension are trivial above some real upper index.
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace ClassFieldTheoryLean source · statement
theorem upperRamificationGroup_eventually_bot
(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 : ℝ, ∀ t : ℝ, T ≤ t → upperRamificationGroup K L t = ⊥