Yamaguchi26AbfaithfulGalois.exists_primePower_character_of_not_pow
Failure of divisibility by a prime power is detected by a continuous character of prime-power order.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace Yamaguchi26AbfaithfulGalois
open ProCGroups ProCGroups.ProC ProCGroups.Abelian
universe uLean source · statement
theorem exists_primePower_character_of_not_pow
{A : Type u} [CommGroup A] [TopologicalSpace A] [IsTopologicalGroup A]
[CompactSpace A] [T2Space A] [TotallyDisconnectedSpace A]
(p : ℕ) [Fact p.Prime] (s : ℕ) (a : A)
(ha : ¬ ∃ b : A, b ^ (p ^ s) = a) :
∃ n : ℕ, 0 < n ∧ ∃ χ : A →ₜ* Multiplicative (ZMod (p ^ n)), χ a ≠ 1