Commit 2024-06-20 17:25 99cf0930

View on Github →

feat: 0 < c * a * star c in StarOrderedRings (#13975) This is a prerequisite for showing when diagonal matrices are positive definite. Missed from #13748

Estimated changes

added theorem conjugate_lt_conjugate
added theorem conjugate_pos'
added theorem conjugate_pos