theorem SymmetricMatrixProperties.isHermitian_iff_transpose_eq {n : Type u_1} (M : Matrix n n ℝ) : M.IsHermitian ↔ M.transpose = M

theorem SymmetricMatrixProperties.eigenvectors_orthogonal_of_ne_eigenvalues {n : Type u_1} [Fintype n] {M : Matrix n n ℝ} (hM : M.IsHermitian) {v w : n → ℝ} {μ₁ μ₂ : ℝ} (hμ : μ₁ ≠ μ₂) (hv : M.mulVec v = μ₁ • v) (hw : M.mulVec w = μ₂ • w) : v ⬝ᵥ w = 0

theorem SymmetricMatrixProperties.eigenvector_linear_combination {n : Type u_1} [Fintype n] {M : Matrix n n ℝ} {v w : n → ℝ} {μ : ℝ} (hv : M.mulVec v = μ • v) (hw : M.mulVec w = μ • w) (a b : ℝ) : M.mulVec (a • v + b • w) = μ • (a • v + b • w)

theorem SymmetricMatrixProperties.exists_orthonormalBasis_eigenvectors {n : Type u_1} [Fintype n] [DecidableEq n] (M : Matrix n n ℝ) (hM : M.IsHermitian) : ∃ (v : OrthonormalBasis n ℝ (EuclideanSpace ℝ n)) (eigvals : n → ℝ), ∀ (j : n), M.mulVec (v j).ofLp = eigvals j • (v j).ofLp

theorem SymmetricMatrixProperties.eq_eigenvectorUnitary_mul_diagonal_mul_transpose {n : Type u_1} [Fintype n] [DecidableEq n] (M : Matrix n n ℝ) (hM : M.IsHermitian) : M = ↑hM.eigenvectorUnitary * Matrix.diagonal hM.eigenvalues * (↑hM.eigenvectorUnitary).transpose

theorem SymmetricMatrixProperties.proposition2_symmetric_matrix {n : Type u_1} [Fintype n] [DecidableEq n] (M : Matrix n n ℝ) (hM : M.IsHermitian) : (∀ {v w : n → ℝ} {μ₁ μ₂ : ℝ}, μ₁ ≠ μ₂ → M.mulVec v = μ₁ • v → M.mulVec w = μ₂ • w → v ⬝ᵥ w = 0) ∧ (∀ {v w : n → ℝ} {μ : ℝ}, M.mulVec v = μ • v → M.mulVec w = μ • w → ∀ (a b : ℝ), M.mulVec (a • v + b • w) = μ • (a • v + b • w)) ∧ (∃ (v : OrthonormalBasis n ℝ (EuclideanSpace ℝ n)) (eigvals : n → ℝ), ∀ (j : n), M.mulVec (v j).ofLp = eigvals j • (v j).ofLp) ∧ M = ↑hM.eigenvectorUnitary * Matrix.diagonal hM.eigenvalues * (↑hM.eigenvectorUnitary).transpose