Mathlib Changelog
v4
Changelog
About
Github
Theorem
Real.not_differentiableAt_rpow_const_zero
Modification history
2025-11-28 10:54
Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean
feat(Analysis): generalize `Real.deriv_rpow_const` and prove iteration version (#32196) …
Added
Real.not_differentiableAt_rpow_const_zero
View on Github →