Theorem Matrix.PosDef.mul_mul_conjTranspose_same

Modification history

2025-04-12 23:32
Mathlib/LinearAlgebra/Matrix/PosDef.lean
feat(LinearAlgebra/Matrix/PosDef): results about conjTranspose (#23895)
Added Matrix.PosDef.mul_mul_conjTranspose_sameView on Github →