pi_n of the n-sphere is Z

pin_sphere_n_mulEquiv_int

Submitter: Kim Morrison.

Notes: The diagonal sphere homotopy-group computation pi_n(S^n) = Z for n at least 1.

Source: Classical theorem in algebraic topology.

Informal solution: Identify homotopy classes of self-maps of S^n with their degree.

theorem declaration uses `sorry`pin_sphere_n_mulEquiv_int (n : ℕ)
    (x : Metric.sphere (0 : EuclideanSpace ℝ (Fin (n + 2))) 1) :
    Nonempty
      (HomotopyGroup.Pi (n + 1) (Metric.sphere (0 : EuclideanSpace ℝ (Fin (n + 2))) 1) x ≃*
        Multiplicative ℤ) := byn:ℕx:↑(Metric.sphere 0 1)⊢ Nonempty (HomotopyGroup.Pi (n + 1) (↑(Metric.sphere 0 1)) x ≃* Multiplicative ℤ)
  sorryAll goals completed! 🐙

Solved by

Not yet solved.