Commit 2024-10-10 16:56 3ae6376f

View on Github →

chore: rename leftovers from the port (#17619)

Estimated changes

Modified Mathlib/Analysis/Calculus/ContDiff/Basic.lean

added theorem ContDiff.comp_contDiffOn₂

added theorem ContDiff.comp_contDiffOn₃

deleted theorem ContDiff.comp_contDiff_on₂

deleted theorem ContDiff.comp_contDiff_on₃

Modified Mathlib/Analysis/Calculus/ContDiff/Bounds.lean

Modified Mathlib/Analysis/Calculus/ContDiff/Defs.lean

added theorem ContDiffWithinAt.differentiableWithinAt'

deleted theorem ContDiffWithinAt.differentiable_within_at'

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

Modified Mathlib/Geometry/Manifold/MFDeriv/Defs.lean

added theorem differentiableWithinAt_localInvariantProp

deleted theorem differentiable_within_at_localInvariantProp