Theorem Matrix.isHermitian_conjTranspose_mul_self

Modification history

2025-11-10 21:47
Mathlib/LinearAlgebra/Matrix/Hermitian.lean
chore(LinearAlgebra/Matrix/Hermitian): fix lemma name (#31484) …
Added Matrix.isHermitian_conjTranspose_mul_selfView on Github →