Theorem Matrix.IsUnit.posSemidef_star_left_conjugate_iff

Modification history

2025-11-05 17:51
Mathlib/LinearAlgebra/Matrix/PosDef.lean
chore: rename **conjugate** to **star_left_conjugate** (#30692) …
Added Matrix.IsUnit.posSemidef_star_left_conjugate_iffView on Github →