Theorem CStarAlgebra.isStrictlyPositive_TFAE

Modification history

2026-10-28 08:06

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

chore: decapitalize `TFAE` in theorem names (#45348) …

Deleted CStarAlgebra.isStrictlyPositive_TFAE View on Github →

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_TFAE View on Github →