ThmDex – An index of mathematical definitions, results, and conjectures.
 ▼ Set of symbols ▼ Alphabet ▼ Deduction system ▼ Theory ▼ Zermelo-Fraenkel set theory ▼ Set ▼ Binary cartesian set product ▼ Binary relation ▼ Map ▼ Countable map ▼ Array ▼ Matrix ▼ Square matrix ▼ Complex square matrix ▼ Invertible complex matrix
Definition D5871
Invertible real matrix

Let $I_N \in \mathbb{R}^{N \times N}$ be a D5621: Real identity matrix.
A D4571: Real matrix $A \in \mathbb{R}^{N \times N}$ is invertible if and only if
 (1) $$\exists \, B \in \mathbb{R}^{N \times N} : B A = I_N$$ (2) $$\exists \, C \in \mathbb{R}^{N \times N} : A C = I_N$$

Let $I_N \in \mathbb{R}^{N \times N}$ be a D5621: Real identity matrix.
A D4571: Real matrix $A \in \mathbb{R}^{N \times N}$ is invertible if and only if
 (1) $A$ is a D5869: Left-invertible real matrix (2) $A$ is a D5868: Right-invertible real matrix
Results
 ▶ R5508: Real square matrix invertible iff determinant nonzero ▶ R5471: Real square matrix invertible iff transpose is ▶ R5500: Transpose of real matrix inverse is inverse to the transpose