[Merged by Bors] - refactor(LinearAlgebra/Matrix/PosDef): Generalize to StarOrderedRing

[eric-wieser]

I assume this is mathematically sound, though right now we can't generalize many dependencies due to the reliance of InnerProductSpace.

---

• depends on: [Merged by bors] - chore(Data/IsROrC/Basic): trivial lemmas about inequalities with zero #6488

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• [Merged by bors] - chore(Data/IsROrC/Basic): trivial lemmas about inequalities with zero #6488
  By Dependent Issues (🤖). Happy coding!

[j-loreaux]

Yes, this is mathematically sound. See, for instance, Takesaki's Theory of Operator Algebras, Volume 1, Lemma IV.3.2 where it is shown that a matrix with entries in a C⋆-algebra is positive (i.e., 0 ≤ with the order structure associated to the C⋆-algebra structure on those matrices) if and only if the matrix is positive semidefinite in the sense given in this PR. In fact, when I eventually get around to putting a (scoped) C⋆-algebra structure on matrices with entries in a C⋆-algebra, positive semidefiniteness is the order structure I'll use.

[j-loreaux]

Unrelated to this PR: I was surprised to find that CommRing is actually necessary here. And that's because it's necessary for, at least, A⁻¹. That's a bit of a shame, because all this 2x2 Schur complement stuff (not involving determinants) should work in the non-commutative setting too (IIRC).

[j-loreaux]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style