Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-19 03:29 150b8e81

View on Github →

feat(analysis/calculus): generalize differentiable*.pow, add differentiable*.zpow (#15416)

Estimated changes

deleted theorem differentiable.pow
added theorem differentiable.zpow
deleted theorem differentiable_at.pow
added theorem differentiable_at.zpow
deleted theorem differentiable_on.pow
added theorem differentiable_on.zpow
added theorem differentiable.pow
added theorem differentiable_at.pow
added theorem differentiable_on.pow