Hopf problem: elliptic · core 6 #
Supporting definitions and proofs for this stage of the six-sphere construction.
theorem
Mathoverflow1973.Elliptic.LogGauge.fundamentalGroup_cast_loop
{Y : Type u_1}
[TopologicalSpace Y]
{a b : Y}
(h : a = b)
(γ : Path a a)
: