Commit 2023-05-29 13:15 ef6c15a1

View on Github →

feat: port LinearAlgebra.Matrix.Hermitian (#4467)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/Matrix/Hermitian.lean

added theorem Matrix.IsHermitian.add

added theorem Matrix.IsHermitian.adjugate

added theorem Matrix.IsHermitian.apply

added theorem Matrix.IsHermitian.coe_re_apply_self

added theorem Matrix.IsHermitian.coe_re_diag

added theorem Matrix.IsHermitian.conjTranspose

added theorem Matrix.IsHermitian.eq

added theorem Matrix.IsHermitian.ext

added theorem Matrix.IsHermitian.ext_iff

added theorem Matrix.IsHermitian.fromBlocks

added theorem Matrix.IsHermitian.inv

added theorem Matrix.IsHermitian.map

added theorem Matrix.IsHermitian.neg

added theorem Matrix.IsHermitian.sub

added theorem Matrix.IsHermitian.submatrix

added theorem Matrix.IsHermitian.transpose

added def Matrix.IsHermitian

added theorem Matrix.isHermitian_add_transpose_self

added theorem Matrix.isHermitian_conjTranspose_iff

added theorem Matrix.isHermitian_conjTranspose_mul_mul

added theorem Matrix.isHermitian_diagonal

added theorem Matrix.isHermitian_diagonal_of_self_adjoint

added theorem Matrix.isHermitian_fromBlocks_iff

added theorem Matrix.isHermitian_iff_isSymmetric

added theorem Matrix.isHermitian_inv

added theorem Matrix.isHermitian_mul_conjTranspose_self

added theorem Matrix.isHermitian_mul_mul_conjTranspose

added theorem Matrix.isHermitian_one

added theorem Matrix.isHermitian_submatrix_equiv

added theorem Matrix.isHermitian_transpose_add_self

added theorem Matrix.isHermitian_transpose_iff

added theorem Matrix.isHermitian_transpose_mul_self

added theorem Matrix.isHermitian_zero