Commit 2024-04-09 19:25 b5b45d35

feat: add the Loewner partial order on continuous linear maps on a Hilbert space (#12026) The (Loewner) partial order on continuous linear maps on a Hilbert space determined by f ≤ g if and only if g - f is a positive linear map (in the sense of ContinuousLinearMap.IsPositive). With this partial order, the continuous linear maps form a StarOrderedRing.