LocalClassFieldTheory.unramifiedNormSubgroup_inf_padicPrincipalSubgroup_le
The intersection of the degree-f unramified condition and the depth-n principal-unit condition is contained in the standard p-adic subgroup with prime exponent f.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory
open LocalFieldTheory.Padic
open LocalFieldTheory.IsNonarchimedeanLocalFieldLean source · statement
theorem unramifiedNormSubgroup_inf_padicPrincipalSubgroup_le
(p f n : ℕ) [Fact p.Prime]
[IsNonarchimedeanLocalField ℚ_[p]] :
unramifiedNormSubgroup ℚ_[p] f ⊓
LocalFieldTheory.uniformizerPrincipalSubgroup ℚ_[p] (padicPrimeUnit p) 1 n ≤
LocalFieldTheory.uniformizerPrincipalSubgroup ℚ_[p] (padicPrimeUnit p) f n