PadicInt.surjective_character_of_nonzero_reduction
A compact-group character in the additive p-adic integers is surjective when its reduction modulo p is nonzero. Its closed image contains the dense integer multiples of a p-adic unit.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace PadicInt
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [CompactSpace G]Lean source · statement
theorem surjective_character_of_nonzero_reduction
(χ : G →ₜ* Multiplicative (PadicInt p))
(hχ : ∃ g : G, toZModPow 1 (χ g).toAdd ≠ 0) :
Function.Surjective χ