In the statement of the Implicit Function Theorem from Rudin, we are asked to assume as a condition that for some function: $$ f: \mathbb{R}^{m+n} \rightarrow \mathbb{R}^n$$ The derivative at some point $Df(x)$ is invertible.
My question is about the invertibility of this non-square matrix. We can see that $Df(x)$ is a linear operator from $\mathbb{R}^{n + m}$ to $\mathbb{R}^n$ so so its matrix representation is not square. This would mean that the the determinant is not defined and hence the definition of invertiblity does not apply. However, $Df(x)$ is still a linear mapping so it would make sense for us to talk about this function as having an inverse when it is 1-to-1 and onto.
Just by visualizing the 1-dimensional case, my intuition says that this would be the case whenever $Df(x) \neq 0$. The proof for such a claim doesn't seem difficult but I was wondering if someone could contribute some clarification for the distinctions between these two definitions and how they relate to the Implicit Function Theorem.
I write an vector of the domain of $f$ as $(x,y)\in\mathbb R^{m+n}$ with $x\in \mathbb R^m$ and $y\in \mathbb R^n$. In the implicit matrix theorem you investigate the Jacobian matrix
$$DF = \frac{\partial F}{\partial (x, y)} = \frac{\partial (F_1,\dots,F_n)}{\partial(x_1,\dots,x_m,y_1,\dots,y_n)} = \begin{pmatrix} \frac{\partial F_1}{\partial x_1} & \cdots & \frac{\partial F_1}{\partial x_m} & \frac{\partial F_1}{\partial y_1} & \cdots & \frac{\partial F_1}{\partial y_n} \\ \vdots & & \vdots &\vdots & & \vdots \\ \frac{\partial F_n}{\partial x_1} & \cdots & \frac{\partial F_n}{\partial x_m} & \frac{\partial F_n}{\partial y_1} & \cdots & \frac{\partial F_n}{\partial y_n} \end{pmatrix}$$
consisting of the two "submatrices":
$$\frac{\partial F}{\partial x} = \frac{\partial (F_1,\dots,F_n)}{\partial(x_1,\dots,x_m)} = \begin{pmatrix} \frac{\partial F_1}{\partial x_1} & \cdots & \frac{\partial F_1}{\partial x_m} \\ \vdots & & \vdots \\ \frac{\partial F_n}{\partial x_1} & \cdots & \frac{\partial F_n}{\partial x_m} \end{pmatrix} $$
and
$$\frac{\partial F}{\partial y} = \frac{\partial (F_1,\dots,F_n)}{\partial(y_1,\dots,y_n)} = \begin{pmatrix} \frac{\partial F_1}{\partial y_1} & \cdots & \frac{\partial F_1}{\partial y_n} \\ \vdots & & \vdots \\ \frac{\partial F_n}{\partial y_1} & \cdots & \frac{\partial F_n}{\partial y_n} \end{pmatrix}$$
The later one is always a square matrix and need to be invertible (not the whole Jacobian!)