Commit 2025-04-12 23:32 dafc764f

View on Github →

feat(LinearAlgebra/Matrix/PosDef): results about conjTranspose (#23895)

Estimated changes

Modified Mathlib/LinearAlgebra/Matrix/PosDef.lean

added theorem Matrix.PosDef.conjTranspose

added theorem Matrix.PosDef.conjTranspose_mul_mul_same

added theorem Matrix.PosDef.mul_mul_conjTranspose_same

added theorem Matrix.PosDef.transpose_iff

added theorem Matrix.posDef_conjTranspose_iff

added theorem Matrix.posSemidef_conjTranspose_iff

added theorem Matrix.posSemidef_transpose_iff