Commit 2024-11-12 02:53 4023a183

chore: split IntegralCurve (#18833) Split Mathlib.Geometry.Manifold.IntegralCurve into three files:

• Mathlib.Geometry.Manifold.IntegralCurve.Basic: Definitions and basic lemmas about continuity and derivatives of integral curves
• Mathlib.Geometry.Manifold.IntegralCurve.Transform: Lemmas about translation and scaling of the domain of integral curves by a constant
• Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique: Local existence and uniqueness theorems for integral curves No content has been substantively changed from the original file. This is to prepare for #9013, which proves a sufficient condition for global existence of integral curves. That'll go in another new file.