Theorem Matrix.isHermitian_iff_isSelfAdjoint

Modification history

2025-10-18 19:47
Mathlib/LinearAlgebra/Matrix/Hermitian.lean
feat(LinearAlgebra/Matrix/PosDef): kronecker of positive (semi-)definite matrices is positive (semi-)definite (#28097) …
Added Matrix.isHermitian_iff_isSelfAdjointView on Github →