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_exists_isUnit_and_isSelfAdjoint_and_eq_mul_self