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