Commit 2025-08-13 22:41 89b7100a

View on Github →

chore: rename IsIntegralCurve to IsMIntegralCurve (#26563) I rename all the existing IsIntegralCurve series of definitions and lemmas for manifolds to IsMIntegralCurve in preparation for reusing IsIntegralCurve for the vector space version.

depends on: #26533

Estimated changes

Modified Mathlib/Geometry/Manifold/IntegralCurve/Basic.lean

deleted theorem IsIntegralCurve.continuous

deleted theorem IsIntegralCurve.isIntegralCurveAt

deleted theorem IsIntegralCurve.isIntegralCurveOn

deleted def IsIntegralCurve

deleted theorem IsIntegralCurveAt.continuousAt

deleted theorem IsIntegralCurveAt.eventually_hasDerivAt

deleted theorem IsIntegralCurveAt.hasMFDerivAt

deleted theorem IsIntegralCurveAt.isIntegralCurveOn

deleted def IsIntegralCurveAt

deleted theorem IsIntegralCurveOn.continuousOn

deleted theorem IsIntegralCurveOn.continuousWithinAt

deleted theorem IsIntegralCurveOn.hasDerivWithinAt

deleted theorem IsIntegralCurveOn.isIntegralCurveAt

deleted theorem IsIntegralCurveOn.mono

deleted def IsIntegralCurveOn

added theorem IsMIntegralCurve.continuous

added theorem IsMIntegralCurve.isMIntegralCurveAt

added theorem IsMIntegralCurve.isMIntegralCurveOn

added def IsMIntegralCurve

added theorem IsMIntegralCurveAt.continuousAt

added theorem IsMIntegralCurveAt.eventually_hasDerivAt

added theorem IsMIntegralCurveAt.hasMFDerivAt

added theorem IsMIntegralCurveAt.isMIntegralCurveOn

added def IsMIntegralCurveAt

added theorem IsMIntegralCurveOn.continuousOn

added theorem IsMIntegralCurveOn.continuousWithinAt

added theorem IsMIntegralCurveOn.hasDerivWithinAt

added theorem IsMIntegralCurveOn.isMIntegralCurveAt

added theorem IsMIntegralCurveOn.mono

added def IsMIntegralCurveOn

deleted theorem isIntegralCurveAt_iff'

deleted theorem isIntegralCurveAt_iff

deleted theorem isIntegralCurveOn_iff_isIntegralCurveAt

deleted theorem isIntegralCurve_iff_isIntegralCurveAt

deleted theorem isIntegralCurve_iff_isIntegralCurveOn

added theorem isMIntegralCurveAt_iff'

added theorem isMIntegralCurveAt_iff

added theorem isMIntegralCurveOn_iff_isMIntegralCurveAt

added theorem isMIntegralCurve_iff_isMIntegralCurveAt

added theorem isMIntegralCurve_iff_isMIntegralCurveOn

Modified Mathlib/Geometry/Manifold/IntegralCurve/ExistUnique.lean

deleted theorem IsIntegralCurve.periodic_of_eq

deleted theorem IsIntegralCurve.periodic_xor_injective

added theorem IsMIntegralCurve.periodic_of_eq

added theorem IsMIntegralCurve.periodic_xor_injective

deleted theorem exists_isIntegralCurveAt_of_contMDiffAt

deleted theorem exists_isIntegralCurveAt_of_contMDiffAt_boundaryless

added theorem exists_isMIntegralCurveAt_of_contMDiffAt

added theorem exists_isMIntegralCurveAt_of_contMDiffAt_boundaryless

deleted theorem isIntegralCurveAt_eventuallyEq_of_contMDiffAt

deleted theorem isIntegralCurveAt_eventuallyEq_of_contMDiffAt_boundaryless

deleted theorem isIntegralCurveOn_Ioo_eqOn_of_contMDiff

deleted theorem isIntegralCurveOn_Ioo_eqOn_of_contMDiff_boundaryless

deleted theorem isIntegralCurve_Ioo_eq_of_contMDiff_boundaryless

deleted theorem isIntegralCurve_eq_of_contMDiff

added theorem isMIntegralCurveAt_eventuallyEq_of_contMDiffAt

added theorem isMIntegralCurveAt_eventuallyEq_of_contMDiffAt_boundaryless

added theorem isMIntegralCurveOn_Ioo_eqOn_of_contMDiff

added theorem isMIntegralCurveOn_Ioo_eqOn_of_contMDiff_boundaryless

added theorem isMIntegralCurve_Ioo_eq_of_contMDiff_boundaryless

added theorem isMIntegralCurve_eq_of_contMDiff

Modified Mathlib/Geometry/Manifold/IntegralCurve/Transform.lean

deleted theorem IsIntegralCurve.comp_add

deleted theorem IsIntegralCurve.comp_mul

deleted theorem IsIntegralCurveAt.comp_add

deleted theorem IsIntegralCurveAt.comp_mul_ne_zero

deleted theorem IsIntegralCurveOn.comp_add

deleted theorem IsIntegralCurveOn.comp_mul

added theorem IsMIntegralCurve.comp_add

added theorem IsMIntegralCurve.comp_mul

added theorem IsMIntegralCurveAt.comp_add

added theorem IsMIntegralCurveAt.comp_mul_ne_zero

added theorem IsMIntegralCurveOn.comp_add

added theorem IsMIntegralCurveOn.comp_mul

deleted theorem isIntegralCurveAt_comp_add

deleted theorem isIntegralCurveAt_comp_mul_ne_zero

deleted theorem isIntegralCurveAt_comp_sub

deleted theorem isIntegralCurveOn_comp_add

deleted theorem isIntegralCurveOn_comp_mul_ne_zero

deleted theorem isIntegralCurveOn_comp_sub

deleted theorem isIntegralCurve_comp_add

deleted theorem isIntegralCurve_comp_mul_ne_zero

deleted theorem isIntegralCurve_comp_sub

deleted theorem isIntegralCurve_const

added theorem isMIntegralCurveAt_comp_add

added theorem isMIntegralCurveAt_comp_mul_ne_zero

added theorem isMIntegralCurveAt_comp_sub

added theorem isMIntegralCurveOn_comp_add

added theorem isMIntegralCurveOn_comp_mul_ne_zero

added theorem isMIntegralCurveOn_comp_sub

added theorem isMIntegralCurve_comp_add

added theorem isMIntegralCurve_comp_mul_ne_zero

added theorem isMIntegralCurve_comp_sub

added theorem isMIntegralCurve_const

Modified Mathlib/Geometry/Manifold/IntegralCurve/UniformTime.lean

deleted theorem eqOn_abs_add_one_of_isIntegralCurveOn_Ioo

added theorem eqOn_abs_add_one_of_isMIntegralCurveOn_Ioo

deleted theorem eqOn_of_isIntegralCurveOn_Ioo

added theorem eqOn_of_isMIntegralCurveOn_Ioo

deleted theorem eqOn_piecewise_of_isIntegralCurveOn_Ioo

added theorem eqOn_piecewise_of_isMIntegralCurveOn_Ioo

deleted theorem exists_isIntegralCurve_iff_exists_isIntegralCurveOn_Ioo

deleted theorem exists_isIntegralCurve_of_isIntegralCurveOn

added theorem exists_isMIntegralCurve_iff_exists_isMIntegralCurveOn_Ioo

added theorem exists_isMIntegralCurve_of_isMIntegralCurveOn

deleted theorem isIntegralCurveOn_piecewise

deleted theorem isIntegralCurve_abs_add_one_of_isIntegralCurveOn_Ioo

added theorem isMIntegralCurveOn_piecewise

added theorem isMIntegralCurve_abs_add_one_of_isMIntegralCurveOn_Ioo

Modified docs/overview.yaml