mathlib

4c3e1721 - feat(topology/homotopy/homotopy_group): `group` and `comm_group` instances for `π_n` (#15681)

feat(topology/homotopy/homotopy_group): `group` and `comm_group` instances for `π_n` (#15681) This PR adds: - Group instance for `π_(n+1)` - Commutative group instance for `π_(n+2)` Co-authored-by: Junyan Xu <junyanxu.math@gmail.com> Co-authored-by: Junyan Xu <junyanxumath@gmail.com> Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>