Commit 2025-11-10 21:47 94010558

View on Github →

chore(LinearAlgebra/Matrix/Hermitian): fix lemma name (#31484) Matrix.isHermitian_transpose_mul_self should be Matrix.isHermitian_conjTranspose_mul_self.

Estimated changes

Modified Mathlib/LinearAlgebra/Matrix/Hermitian.lean

added theorem Matrix.isHermitian_conjTranspose_mul_self

deleted theorem Matrix.isHermitian_transpose_mul_self

Modified Mathlib/LinearAlgebra/Matrix/PosDef.lean