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