Jacobi determinant of f?

Stream: Is there code for X?

[Ryan Lahfa]

I'm trying to understand if there is some theory for Jacobi determinants of $C^1$ functions over open set.

More specifically, I'm okay with developing $J_f(x)$ but I wonder if it's "straightforward" to define $\textrm{d}f(x)$ as a matrix, etc. ?

I searched quickly over this stream but found nothing.

[Ryan Lahfa]

Looks like https://leanprover-community.github.io/mathlib_docs/analysis/calculus/fderiv.html#fderiv is the starting point