Theorem LinearMap.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 LinearMap.nonneg_iff_isPositive View on Github →

2025-06-04 13:46

Mathlib/Analysis/InnerProductSpace/Positive.lean

feat: define `IsPositive` and Löwner order for `LinearMap` (#24471) …

Added LinearMap.nonneg_iff_isPositive View on Github →