Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-02 15:58 29415900

View on Github →

feat(linear_algebra/matrix): Spectral theorem for matrices (#14231)

Estimated changes

Modified src/analysis/inner_product_space/pi_L2.lean

added theorem euclidean_space.inner_eq_star_dot_product

Modified src/analysis/normed_space/pi_Lp.lean

added theorem pi_Lp.equiv_apply'

modified theorem pi_Lp.equiv_apply

added theorem pi_Lp.equiv_symm_apply'

modified theorem pi_Lp.equiv_symm_apply

Modified src/linear_algebra/matrix/basis.lean

added theorem basis_to_matrix_basis_fun_mul

added theorem basis_to_matrix_mul

added theorem mul_basis_to_matrix

Created src/linear_algebra/matrix/hermitian.lean

added theorem matrix.conj_transpose_map

added theorem matrix.is_hermitian.add

added theorem matrix.is_hermitian.apply

added theorem matrix.is_hermitian.conj_transpose

added theorem matrix.is_hermitian.eq

added theorem matrix.is_hermitian.ext

added theorem matrix.is_hermitian.ext_iff

added theorem matrix.is_hermitian.from_blocks

added theorem matrix.is_hermitian.map

added theorem matrix.is_hermitian.minor

added theorem matrix.is_hermitian.neg

added theorem matrix.is_hermitian.sub

added theorem matrix.is_hermitian.transpose

added def matrix.is_hermitian

added theorem matrix.is_hermitian_add_transpose_self

added theorem matrix.is_hermitian_diagonal

added theorem matrix.is_hermitian_from_blocks_iff

added theorem matrix.is_hermitian_iff_is_self_adjoint

added theorem matrix.is_hermitian_mul_conj_transpose_self

added theorem matrix.is_hermitian_one

added theorem matrix.is_hermitian_transpose_add_self

added theorem matrix.is_hermitian_transpose_mul_self

added theorem matrix.is_hermitian_zero

Created src/linear_algebra/matrix/spectrum.lean

added theorem matrix.is_hermitian.eigenvector_matrix_mul_inv

added theorem matrix.is_hermitian.spectral_theorem

Modified src/linear_algebra/matrix/to_lin.lean

modified theorem matrix.mul_vec_std_basis

added theorem matrix.mul_vec_std_basis_apply