deriv): make the exponent explicit in pow lemmas (#15117)

Commit

3 years ago

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

Author

sgouezel

Parents

73d15d77

mathlib 18860933 - chore(analysis/calculus/deriv): make the exponent explicit in pow lemmas (#15117)

mathlib
18860933 - chore(analysis/calculus/deriv): make the exponent explicit in pow lemmas (#15117)