Commit 2023-08-04 16:36 b80c0cc9
View on Github →ConjTranspose multiplication of a matrix by itself is Positive Semidefinite (#6359)
This PR provides two lemmas isPosSemidef_conjTranspose_mul_self and isPosSemidef_self_mul_conjTranspose stating that for any matrix $A$ the products $A^HA$ and $AA^H$ in the IsROrC fields are positive semidefinite.