mathlib3
d9fbe9d2 - chore(geometry/manifold/times_cont_mdiff_map): add `times_cont_mdiff_map.mdifferentiable` (#6703)

Commit
4 years ago
chore(geometry/manifold/times_cont_mdiff_map): add `times_cont_mdiff_map.mdifferentiable` (#6703)
Author
Parents
Loading