Mathlib Changelog
v4
Changelog
About
Github
Theorem
ContinuousLinearMap.IsPositive.inner_nonneg_left
Modification history
2023-06-01 14:53
Mathlib/Analysis/InnerProductSpace/Positive.lean
feat: port Analysis.InnerProductSpace.Positive (#4553)
Added
ContinuousLinearMap.IsPositive.inner_nonneg_left
View on Github →