Real Eigenvalues and Eigenvectors of a Real Square Matrix

In the setting of Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices, let $n\in\mathbb{N}$, let $A\in\mathcal{M}_{n}(\mathbb{R})$ be a square real matrix and let $\lambda\in\mathbb{R}$, with the matrix-vector product $Ax$, the scalar multiple $\lambda x$ and the origin $0$ of $\mathbb{R}^{n}$.

¶ A point $x\in\mathbb{R}^{n}$ is an eigenvector of $A$ with eigenvalue $\lambda$ if $x\neq0$ and $Ax=\lambda x$.

¶ $\lambda$ is an eigenvalue of $A$ if $A$ has an eigenvector with eigenvalue $\lambda$.