ProCGroups.exists_prime_power_order_lift_of_surjective
Every element of a finite p-group quotient has a lift of p-power order.
Source context 1 command
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ProCGroupsLean source · statement
theorem exists_prime_power_order_lift_of_surjective
{G H : Type*} [Group G] [Group H] [Finite G]
(p : ℕ) [Fact p.Prime] (f : G →* H) (hf : Function.Surjective f)
(hH : IsPGroup p H) (y : H) :
∃ x : G, f x = y ∧ ∃ n : ℕ, x ^ (p ^ n) = 1