Commit 2023-03-21 19:41 dd6388c4
View on Github →chore(analysis/calculus/cont_diff): split into two files (#18627)
The file cont_diff.lean takes 3824 lines. We cut it into two files, cont_diff_def.lean and cont_diff.lean, the former (of 1597 lines) containing general definitions and the latter (of 2264 lines) containing results on the preservation of smoothness by the usual operations and various API extensions that depend on these.
There is no single change in maths or code, this is purely a split PR.