Hopf problem: period family · core 3 #
Supporting definitions and proofs for this stage of the six-sphere construction.
theorem
Mathoverflow1973.PeriodFamily.freeSemidirect_subgroup_eq_top
{N : Type u_1}
{α : Type u_2}
[Group N]
(φ : FreeGroup α →* MulAut N)
(S : Subgroup (N ⋊[φ] FreeGroup α))
(hN : ∀ (n : N), SemidirectProduct.inl n ∈ S)
(hG : ∀ (a : α), SemidirectProduct.inr (FreeGroup.of a) ∈ S)
: