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_isUnit_sqrt_and_eq_sqrt_mul_sqrt