ThmDex – An index of mathematical definitions, results, and conjectures.

Result R5508 on D5871: Invertible real matrix
Subresult of R5507: Real square matrix invertible iff determinant is

Real square matrix invertible iff determinant nonzero

Formulation 0

Let $A \in \mathbb{R}^{N \times N}$ be a D6160: Real square matrix.

Then the following statements are equivalent

(1)	$A$ is an D5871: Invertible real matrix
(2)	\begin{equation} \text{Det} A \neq 0 \end{equation}

Proofs

Proof 0

Let $A \in \mathbb{R}^{N \times N}$ be a D6160: Real square matrix.

If $x \in \mathbb{R}$ is a real number, then the multiplicative inverse $1 / x$ exists if and only if $x \neq 0$. Hence, this result is a direct consequence to R5507: Real square matrix invertible iff determinant is. $\square$