Theorem IsStrictlyPositive.iff_of_unital

Modification history

2025-09-26 11:53
Mathlib/Algebra/Algebra/StrictPositivity.lean
feat: Define strictly positive operators (i.e. positive definite) (#29087)
Added IsStrictlyPositive.iff_of_unitalView on Github →