Homotopy invariance of the topological degree — unconditional

Now that the singular prism operator is a theorem (singularPrismOperator, established in SingularHomologyHomotopyInvariance.lean from the backported algebraic prism and the library cylinder), the homotopy-invariance wrappers of Degree.lean — which were stated conditionally on SingularPrismOperator — are unconditional.

theorem SphereOddDegree.inducedOnTopHomology_eq_of_homotopic_unconditional {n : ℕ} {f g : C(Sphere n, Sphere n)} (h : f.Homotopic g) : inducedOnTopHomology f = inducedOnTopHomology g

Homotopy invariance of the induced top-homology endomorphism (unconditional). Homotopic self-maps f, g : C(Sphere n, Sphere n) induce the same endomorphism of Hₙ(TopCat.sphere n; ℤ).

theorem SphereOddDegree.degreeOfIso_eq_of_homotopic_unconditional {n : ℕ} (e : (singularHomologyℤ n).obj (TopCat.sphere n) ≅ ↧ℤ) {f g : C(Sphere n, Sphere n)} (h : f.Homotopic g) : degreeOfIso e f = degreeOfIso e g

Homotopy invariance of the degree (unconditional). Homotopic self-maps of Sphere n have equal degree relative to any chosen identification e : Hₙ(Sⁿ; ℤ) ≅ ℤ.