Commit 2025-09-27 15:46 09b236a3

View on Github →

feat(Analysis/SpecialFunctions/CFC/Rpow/Basic): add isStrictlyPositive_TFAE (#30013) Some equivalent lemmas for strict positivity in a C⋆-algebra.

Estimated changes

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

added theorem CStarAlgebra.isStrictlyPositive_TFAE

added theorem CStarAlgebra.isStrictlyPositive_iff_eq_mul_star_self

added theorem CStarAlgebra.isStrictlyPositive_iff_eq_star_mul_self

added theorem CStarAlgebra.isStrictlyPositive_iff_exists_isStrictlyPositive_and_eq_mul_self

added theorem CStarAlgebra.isStrictlyPositive_iff_exists_isUnit_and_isSelfAdjoint_and_eq_mul_self

added theorem CStarAlgebra.isStrictlyPositive_iff_isSelfAdjoint_and_spectrum_pos

added theorem CStarAlgebra.isStrictlyPositive_iff_isStrictlyPositive_sqrt_and_eq_sqrt_mul_sqrt

added theorem CStarAlgebra.isStrictlyPositive_iff_isUnit_sqrt_and_eq_sqrt_mul_sqrt