Theorem ContinuousLinearMap.nonneg_iff_isPositive

Modification history

2026-08-13 18:50

Mathlib/Analysis/InnerProductSpace/Positive.lean

feat(Analysis/InnerProductSpace/Positive): add IsOrderedModule for (Continuous)LinearMaps (#42680) …

Modified ContinuousLinearMap.nonneg_iff_isPositive View on Github →

2024-04-09 19:25

Mathlib/Analysis/InnerProductSpace/Positive.lean

feat: add the Loewner partial order on continuous linear maps on a Hilbert space (#12026) …

Added ContinuousLinearMap.nonneg_iff_isPositive View on Github →