proposition: Theorem pi1_s1 : Pi 1 (psphere 1) ≅ abgroup_Z.
proof: Proof. etransitivity. 2: apply pi1_circle. apply groupiso_pi_functor. apply pequiv_S1_Circle. Defined.
imports: Basics Types WildCat Pointed Truncations.Core Truncations.Connectedness Spaces.Int Spaces.Circle Spaces.Spheres Algebra.AbGroups Homotopy.HomotopyGroup Homotopy.HSpaceS1 Homotopy.Hopf