Commit 2022-07-04 23:23 18860933

View on Github →

chore(analysis/calculus/deriv): make the exponent explicit in pow lemmas (#15117) This is useful to build derivatives for explicit functions using dot notation.

Estimated changes

Modified archive/100-theorems-list/9_area_of_a_circle.lean

Modified src/analysis/calculus/deriv.lean

modified theorem deriv_pow'

modified theorem deriv_pow

Modified src/analysis/complex/phragmen_lindelof.lean

Modified src/analysis/convex/specific_functions.lean

Modified src/analysis/special_functions/integrals.lean