times_cont_diff): smoothness of `f : E → Π i, F i` (#6674)

Commit

5 years ago

feat(analysis/calculus/times_cont_diff): smoothness of `f : E → Π i, F i` (#6674) Also add helper lemmas/definitions about multilinear maps.

Author

urkud

Parents