Theorem Matrix.IsUnit.posSemidef_conjugate_iff'

Modification history

2025-11-05 17:51

Mathlib/LinearAlgebra/Matrix/PosDef.lean

chore: rename **conjugate** to **star_left_conjugate** (#30692) …

Deleted Matrix.IsUnit.posSemidef_conjugate_iff'View on Github →

2025-10-18 19:47

Mathlib/LinearAlgebra/Matrix/PosDef.lean

feat(LinearAlgebra/Matrix/PosDef): kronecker of positive (semi-)definite matrices is positive (semi-)definite (#28097) …

Added Matrix.IsUnit.posSemidef_conjugate_iff'View on Github →