ThmDex – An index of mathematical definitions, results, and conjectures.
Formulation 0
Let $f : \mathbb{R}^{N \times M} \to \mathbb{R}^{K \times M}$ be a D5655: Real matrix function such that
(i) \begin{equation} \exists \, A \in \mathbb{R}^{N \times K} \text{ and } B \in \mathbb{R}^{K \times M} : \forall \, X \in \mathbb{R}^{N \times M} : f(X) = A^T X + B \end{equation}
Let $L : \mathbb{R}^{N \times M} \to \mathbb{R}^{K \times M}$ be a D5655: Real matrix function such that
(i) \begin{equation} \forall \, X \in \mathbb{R}^{N \times M} : L(X) = A^T X \end{equation}
Then $L$ is a D5787: Real matrix function derivative for $f$ on $\mathbb{R}^{N \times M}$.
Proofs
Proof 0
Let $f : \mathbb{R}^{N \times M} \to \mathbb{R}^{K \times M}$ be a D5655: Real matrix function such that
(i) \begin{equation} \exists \, A \in \mathbb{R}^{N \times K} \text{ and } B \in \mathbb{R}^{K \times M} : \forall \, X \in \mathbb{R}^{N \times M} : f(X) = A^T X + B \end{equation}
Let $L : \mathbb{R}^{N \times M} \to \mathbb{R}^{K \times M}$ be a D5655: Real matrix function such that
(i) \begin{equation} \forall \, X \in \mathbb{R}^{N \times M} : L(X) = A^T X \end{equation}
This result is a particular case of R4914: Derivative for an affine real matrix function. $\square$