Theorem Matrix.PosDef.conjTranspose_mul_mul_same

Modification history

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