Theorem Matrix.posSemidef_transpose_iff

Modification history

2025-08-31 08:11
Mathlib/LinearAlgebra/Matrix/PosDef.lean
chore: generalize `Matrix.PosDef` to non-commutative rings (#29150) …
Modified Matrix.posSemidef_transpose_iffView on Github →
2025-04-12 23:32
Mathlib/LinearAlgebra/Matrix/PosDef.lean
feat(LinearAlgebra/Matrix/PosDef): results about conjTranspose (#23895)
Added Matrix.posSemidef_transpose_iffView on Github →