QuantumInfo.ForMathlib.HermitianMat.NonSingular

Let $R$ and $S$ be rings, and let $M$ be a $d \times d$ square matrix over $S$. If $c \in R$ is a unit and $M$ is an invertible matrix (i.e., a unit in the matrix ring), then the scalar product $c \cdot M$ is also an invertible matrix.

Let $n$ be a natural number such that $n \neq 0$, and let $F$ be a field with characteristic zero. Then the scalar matrix $n \cdot I$ (the natural number $n$ cast into the space of $d \times d$ matrices over $F$) is a unit in the ring of matrices.

Let $r$ be a real number such that $r \neq 0$, and let $M$ be a $d \times d$ matrix over a field $\mathbb{k}$. If $M$ is an invertible matrix, then the scalar multiple $r \cdot M$ is also an invertible matrix.

Let $r$ be a real number such that $r \neq 0$. In the space of $d \times d$ matrices over a field $\mathbb{k}$, the scalar matrix $r \cdot I$ (where $I$ is the identity matrix) is invertible (an unit).

Given a Hermitian matrix $A$, if $A$ is non-singular, then its underlying matrix $\text{mat}(A)$ is a unit (i.e., it is invertible) in the ring of matrices.

For a Hermitian matrix $A$, $A$ is non-singular if and only if its underlying matrix $A.\text{mat}$ is a unit in the ring of matrices (i.e., it is invertible).

Let $A$ be a Hermitian matrix. If the underlying matrix $A.\text{mat}$ is invertible (i.e., there exists an instance of `Invertible A.mat`), then $A$ is non-singular.

Given a Hermitian matrix $A$ such that it is non-singular (i.e., its underlying matrix $A.mat$ is a unit in the matrix ring), then $A.mat$ is an invertible element.

Let $R$ be a ring and $n$ be a natural number. The identity matrix $1$ in the space of $n \times n$ Hermitian matrices over $R$ is non-singular.

Let $A$ be a Hermitian matrix. If the underlying matrix $A_{\text{mat}}$ is positive definite (denoted as $A_{\text{mat}} \text{.PosDef}$), then $A$ is non-singular.

Let $A$ be a Hermitian matrix such that $A \ge 0$ (i.e., $A$ is positive semidefinite) according to the Loewner partial order. Then, $A$ is non-singular if and only if $A$ is positive definite ($A > 0$).

Let $A$ be a Hermitian matrix and $c$ be a real number. If $A$ is non-singular (i.e., its underlying matrix is invertible) and $c$ is a unit (i.e., $c \neq 0$), then the scalar product $c \cdot A$ is also non-singular.

A Hermitian matrix $A$ is non-singular if and only if zero is not contained in its spectrum $\sigma(A)$, where the spectrum is taken over the real numbers $\mathbb{R}$.

A Hermitian matrix $A$ is non-singular if and only if all of its eigenvalues $\lambda_i$ are non-zero.

A Hermitian matrix $A$ is non-singular if and only if its determinant is non-zero, $\det(A) \neq 0$.

A Hermitian matrix $A$ is non-singular if and only if its kernel is trivial, denoted as $\ker(A) = \{0\}$ (or $\ker A = \bot$ in the context of submodule lattice).

A Hermitian matrix $A$ is non-singular if and only if its support is the top element of the subspace lattice (i.e., its support is the entire space), denoted as $\text{support}(A) = \top$.

For a Hermitian matrix $A$, the matrix $-A$ is non-singular if and only if $A$ is non-singular.

A Hermitian matrix $A^{-1}$ is nonsingular if and only if the Hermitian matrix $A$ is nonsingular. Here, $A^{-1}$ denotes the matrix inverse of $A$.

Let $A$ and $B$ be Hermitian matrices indexed by non-empty types $n$ and $m$ respectively. The Kronecker product $A \otimes_k B$ is non-singular if and only if both $A$ and $B$ are non-singular.

Let $A$ be a Hermitian matrix and $C$ be an invertible matrix (i.e., $C$ is a unit). Then the congruence transformation of $A$ by $C$, denoted $C^* A C$, is non-singular if and only if $A$ is non-singular.

Let $A$ be a Hermitian matrix indexed by $n$, and let $e: n \simeq m$ be a bijection between index types $n$ and $m$. Let $A.\text{reindex}(e)$ denote the Hermitian matrix indexed by $m$ such that its entries are given by $(A.\text{reindex}(e))_{i, j} = A_{e^{-1}(i), e^{-1}(j)}$. Then $A.\text{reindex}(e)$ is non-singular if and only if $A$ is non-singular.

Let $A$ be a Hermitian matrix of size $n \times n$. If the index set $n$ is empty (i.e., $A$ is a $0 \times 0$ matrix), then $A$ is non-singular.

Let $A$ be a Hermitian matrix. Then the determinant of $A$ is non-zero, denoted as $\det(A) \neq 0$. *(Note: Based on the context of the neighbor statement `HermitianMat.nonSingular_iff_det_ne_zero`, this theorem identifies that a non-singular Hermitian matrix has a non-zero determinant.)*

Let $A$ be a Hermitian matrix. The matrix $A$ is non-singular if and only if its kernel is trivial, denoted as $\ker A = \{0\}$ (or $\text{ker } A = \bot$).

For a Hermitian matrix $A$, if $A$ is non-singular, then its support is the top element of the lattice of subspaces (i.e., the entire space), denoted as $\text{support}(A) = \top$.

Let $A$ be a Hermitian matrix. The negation of the matrix, $-A$, is non-singular.

If a Hermitian matrix $A$ is non-singular, then its inverse $A^{-1}$ is also non-singular.

Let $A$ and $B$ be Hermitian matrices indexed by non-empty sets $n$ and $m$ respectively. Then the Kronecker product $A \otimes_k B$ is non-singular.

Let $A$ be a Hermitian matrix and $C$ be a matrix. If $C$ is an invertible matrix (i.e., it is a unit in the ring of matrices), then the congruence transformation of $A$ by $C$, defined as $A.\text{conj } C$, is a non-singular matrix.

Let $A$ and $B$ be Hermitian matrices of size $n$ over the field $\mathbb{K}$. If $B$ is non-singular, then the congruence transformation (conjugation) of $A$ by the matrix of $B$, denoted as $B A B^*$, is also non-singular.

Let $A$ be a Hermitian matrix. Then $0$ is not contained in the spectrum of $A$ over $\mathbb{R}$, denoted by $0 \notin \sigma(A)$.

For a Hermitian matrix $A$, the matrix is non-singular if and only if all of its eigenvalues $\lambda_i$ are non-zero, i.e., $\forall i, \lambda_i \neq 0$.