mathlib3
c45e70ac - chore(analysis/special_functions/pow): put lemmas about derivatives into a new file (#10153)

Commit
4 years ago
chore(analysis/special_functions/pow): put lemmas about derivatives into a new file (#10153) In order to keep results about continuity of the power function in the original file, we prove some continuity results directly (these were previously proved using derivatives). Co-authored-by: RemyDegenne <remydegenne@gmail.com>
Author
Parents
Loading