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