Theorem isStrictlyPositive_add

Modification history

2025-09-26 11:53

Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean

feat: Define strictly positive operators (i.e. positive definite) (#29087)

Added isStrictlyPositive_add View on Github →