ProCGroups.ProC.eq_one_of_prime_torsion_of_primaryQuotient_eq_one
Elements killed by a prime inject into the maximal pro-prime quotient.
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ProCGroups.ProC
universe uLean source · statement
theorem eq_one_of_prime_torsion_of_primaryQuotient_eq_one
{p : ℕ} [Fact p.Prime]
{A : Type u} [CommGroup A] [TopologicalSpace A] [IsTopologicalGroup A]
[CompactSpace A] [T2Space A] [TotallyDisconnectedSpace A]
(a : A) (ha : a ^ p = 1)
(hπ : QuotientGroup.mk' (proCResidualCore (FiniteGroupClass.pGroup p) A) a = 1) :
a = 1