[Merged by Bors] - feat(topology/homotopy/homotopy_group): group and comm_group instances for π_n

src/topology/homeomorph.lean

@@ -1,4 +1,4 @@
 /-
 Copyright (c) 2019 Reid Barton. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Patrick Massot, Sébastien Gouëzel, Zhouhang Zhou, Reid Barton
@@ -504,6 +504,7 @@
   continuous_inv_fun := continuous_pi $ λ j, by { dsimp only [equiv.pi_split_at],
     split_ifs, subst h, exacts [continuous_fst, (continuous_apply _).comp continuous_snd] } }
 
+variable (β)
 /-- A product of copies of a topological space can be split as the binary product of one copy and
   the product of all the remaining copies. -/
 @[simps] def fun_split_at : (ι → β) ≃ₜ β × ({j // j ≠ i} → β) := pi_split_at i _