mathlib

f93c1193 - feat(geometry/manifold/mfderiv): more arithmetic (#17793)

feat(geometry/manifold/mfderiv): more arithmetic (#17793) * generalize most arithmetic from normed algebra to normed space * add some arithmetic with `mfderiv` * redefine `mfderiv` (and variants) to use `if` instead of dependent `if`.