Commit 2021-11-04 00:15 0fac0807
View on Github →refactor(analysis/calculus/mean_value): Remove useless hypotheses (#10129)
Because the junk value of deriv is 0, assuming ∀ x, 0 < deriv f x implies that f is derivable. We thus remove all those redundant derivability assumptions.