Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-13 11:53 7697ec6e

View on Github →

feat(analysis/special_function/integrals): integral of x ^ r, r : ℝ, and x ^ n, n : ℤ (#10650) Also generalize has_deriv_at.div_const etc.

Estimated changes

modified theorem deriv_div_const
modified theorem deriv_within_div_const
modified theorem differentiable.div_const
modified theorem differentiable_at.div_const
modified theorem differentiable_on.div_const
added theorem has_deriv_at.div_const
modified theorem integral_pow
added theorem integral_rpow
added theorem integral_zpow
modified theorem real.rpow_int_cast
modified theorem real.rpow_nat_cast