Commit 2023-08-09 21:32 3e8bc7b2
View on Github →feat: Rank of a hermitian matrix is the count of non-zero eigenvalues (#6354) This PR provides the lemmas:
IsHermitian.spectral_theorem': a slightly modified spectral_theorem such that the hermitian matrix can be directly replaced. $$A = VDV^{-1}\quad D = \text{diag}(d)$$IsHermitian.rank_eq_count_non_zero_eigs: the rank of a hermitian matrix is the number of non-zero eigenvalues of that matrix $$\text{rank}(A) = \text{card} \lbrace \quad i \quad | \quad d_i \neq 0 \rbrace$$IsHermitian.rank_eq_rank_diagonal: the rank of a hermitian matrix is the same as its rank after diagonalization by the eigenvector matrix $$\text{rank}(A) = \text{rank}(D)$$Matrix.rank_diagonal: the rank of a diagonal matrix is the number of non-zero diagonal elements. Note that this was previously the name of a lemma about LinearMaps we take that name (but keep the align to avoid disrupting the tooling). $$\text{rank}(V) = \text{Diag}(v) \implies \text{rank}(V) = \text{card} \lbrace \quad i \quad | \quad v_i \neq 0 \rbrace$$LinearMap.rank_diagonal: the rank of a linear map that is formed from a diagonal matrix is the number of non-zero diagonal entries. This was previously calledMatrix.rank_diagonal.