mathlib

3600b621 - feat(topology/homotopy): define nth homotopy group πₙ (without the group instance) (#14724)

feat(topology/homotopy): define nth homotopy group πₙ (without the group instance) (#14724) This pull request adds: - definition of the nth homotopy group `π n x` - proof of `π 0 x ≃ zeroth_homotopy X` where `x:X` - proof of `π 1 x ≃ path.homotopic.quotient x x` Co-authored-by: Junyan Xu <junyanxumath@gmail.com> Co-authored-by: Roberto Álvarez <roberto.alvz3@gmail.com>