Kurosh Free Part #
Adapted for Lean Pool from Arthur742Ramos/KuroshSubgroupTheorem,
commit 911707126c8b9bb0c764bf853008fe1053c0aad9: imports, API compatibility,
and proof organization were revised.
theorem
GraphCoveringTheory.Kurosh.kuroshFreePartHom_injective
{ι : Type v}
(G : ι → Type u)
[(i : ι) → Group (G i)]
(H : Subgroup (FreeProduct G))
:
The quotient-graph free factor embeds in the subgroup.