Finite embedding problems for free pro-p groups

The universal property solves finite embedding problems with p-group kernel, without a finiteness assumption on the generating type. Thus solvability by itself does not impose topological finite generation.

theorem TauCeti.hasPGroupSolutions_freeProP (p : ℕ) (X : Type u) : HasPGroupSolutions p (freeProP p X)

A free pro-p group solves every finite embedding problem with p-group kernel.