Theorem CStarAlgebra.isStrictlyPositive_iff_eq_mul_star_self

Modification history

2025-09-27 15:46

Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Basic.lean

feat(Analysis/SpecialFunctions/CFC/Rpow/Basic): add `isStrictlyPositive_TFAE` (#30013) …

Added CStarAlgebra.isStrictlyPositive_iff_eq_mul_star_self View on Github →