Commit 2022-08-09 21:53 a5413b69
View on Github →chore(analysis/calculus/cont_diff): Add two helper lemmas (#15894)
This PR adds the forward direction of cont_diff_iff_continuous_differentiable as separate lemmas, which enables using dot-notation for cont_diff.