Commit 2024-11-04 18:42 2f5cf5f5

View on Github →

feat: derivatives of piLp operations (#17665) Zulip thread

Estimated changes

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

added theorem PiLp.hasFDerivAt_equiv

added theorem PiLp.hasFDerivAt_equiv_symm

added theorem PiLp.hasStrictFDerivAt_equiv

added theorem PiLp.hasStrictFDerivAt_equiv_symm