theorem fundamental_group_real_zero_subsingleton : Subsingleton (FundamentalGroup ℝ 0)

Lemma 1.5.1: the fundamental group of ℝ based at 0 is trivial.

theorem fundamental_group_real_zero_eq_one (γ : FundamentalGroup ℝ 0) : γ = 1

Every element of the fundamental group of ℝ at 0 is the identity.