Theorem StarOrderedRing.isStrictlyPositive_iff_spectrum_pos

Modification history

2025-09-26 11:53
Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
feat: Define strictly positive operators (i.e. positive definite) (#29087)
Added StarOrderedRing.isStrictlyPositive_iff_spectrum_posView on Github →