Commit 2025-12-22 11:55 61d1f8fb

View on Github →

refactor(Analysis,Geometry): assume n ≠ 0, not 1 ≤ n (#33131) This way it's a positivity goal.

Estimated changes

modified theorem ContDiff.continuous_fderiv
modified theorem ContDiff.differentiable
modified theorem ContDiffAt.differentiableAt
modified theorem ContDiffOn.differentiableOn
modified theorem ContDiff.hasStrictDerivAt
modified theorem ContDiff.hasStrictFDerivAt
modified theorem ContDiffAt.hasStrictDerivAt
modified theorem ContMDiff.mdifferentiable
modified theorem ContMDiff.mdifferentiableAt