ProCGroups.FiniteGroupClass.eq_one_of_primePower_roots
An element with an ℓ^s-th root for every allowed prime ℓ and positive s is trivial.
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ProCGroups.FiniteGroupClass
universe uLean source · statement
theorem eq_one_of_primePower_roots
{sigma : Set ℕ} {G : Type u} [Group G] [Finite G]
(hG : FiniteGroupClass.sigmaGroup sigma G) (x : G)
(hx : ∀ ℓ : ℕ, ℓ ∈ sigma → ℓ.Prime →
∀ s : ℕ, 0 < s → ∃ y : G, y ^ (ℓ ^ s) = x) : x = 1