Commit 2020-06-22 13:19 86dcd5cd

feat(analysis/calculus): C^1 implies strictly differentiable (#3119) Over the reals, a continuously differentiable function is strictly differentiable. Supporting material: Add a standard mean-value-theorem-related trick as its own lemma, and refactor another proof (in calculus/extend_deriv) to use that lemma. Other material: an equality (rather than inequality) version of the mean value theorem for domains; slight refactor of normed_space/dual.