hopf_umlaufsatz.toml

id = "hopf_umlaufsatz"
title = "The Hopf Umlaufsatz (theorem of turning tangents)"
test = false
module = "LeanEval.Geometry.HopfUmlaufsatz"
holes = ["hopf_umlaufsatz"]
submitter = "Kim Morrison"
notes = "A positively oriented simple closed unit-speed plane curve has total signed curvature 2π. Trusted helpers (signedArea, signedCurvature, totalCurvature, IsPositiveSimpleClosedUnitSpeedCurve, IsTangentAngleLift, …) are non-holes. Mathlib has no turning-tangents theorem. Candidate from §170 of the Knill survey."
source = "H. Hopf, *Über die Drehung der Tangenten...*, Compositio Math. 2 (1935). Knill, §170."