Commit 2023-07-26 09:26 2ae56d8d

View on Github →

feat: derivative of the inversion (#5937) Prove that inversion is smooth away from the center and its derivative is a scaled reflection.

Estimated changes

Modified Mathlib.lean

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

added theorem HasFDerivAt.congr_fderiv

added theorem HasFDerivWithinAt.congr_fderiv

added theorem HasStrictFDerivAt.congr_fderiv

Modified Mathlib/Analysis/InnerProductSpace/Calculus.lean

added theorem HasFDerivAt.norm_sq

added theorem HasFDerivWithinAt.norm_sq

Modified Mathlib/Analysis/InnerProductSpace/Projection.lean

added theorem reflection_singleton_apply

Created Mathlib/Geometry/Euclidean/Inversion/Calculus.lean

added theorem EuclideanGeometry.hasFDerivAt_inversion