Commit 2022-10-29 21:19 2423ed87
View on Github →chore(analysis/calculus/cont_diff): add missing lemmas and golfs (#17233) Adds two trivial lemmas. Moreover, we golf a few proofs and remove non-terminal simps.
chore(analysis/calculus/cont_diff): add missing lemmas and golfs (#17233) Adds two trivial lemmas. Moreover, we golf a few proofs and remove non-terminal simps.