Commit 2021-03-15 15:39 ae776282
View on Github →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.