mathlib

ae776282 - chore(geometry/manifold/times_cont_mdiff): add `prod_mk_space` versions of `prod_mk` lemmas (#6681)

chore(geometry/manifold/times_cont_mdiff): add `prod_mk_space` versions of `prod_mk` lemmas (#6681) These lemmas are useful when dealing with maps `f : M → E' × F'` where `E'` and `F'` are normed spaces. This means some code duplication with `prod_mk` lemmas but I see no way to avoid this without making proofs about `M → E' × F'` longer/harder.