mathlib

e49ac91b - feat(analysis/calculus/cont_diff): add more prod lemmas (#13521)

feat(analysis/calculus/cont_diff): add more prod lemmas (#13521) * Add `cont_diff.fst`, `cont_diff.comp₂`, `cont_diff_prod_mk_left` and many variants. * From the sphere eversion project * Required for convolutions * PR #13423 is similar for continuity