Theorem ContinuousLinearMap.IsPositive.inner_left_eq_inner_right

Modification history

2025-06-04 13:46
Mathlib/Analysis/InnerProductSpace/Positive.lean
feat: define `IsPositive` and Löwner order for `LinearMap` (#24471) …
Added ContinuousLinearMap.IsPositive.inner_left_eq_inner_rightView on Github →