Theorem CStarAlgebra.nonneg_TFAE

Modification history

2026-10-28 08:06

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

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

Deleted CStarAlgebra.nonneg_TFAE View on Github →

2025-09-16 11:11

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

feat(Analysis/SpecialFunctions/CFC/Rpow): `0 ≤ a` iff `a = star b * b` for some `b` (#29592) …

Added CStarAlgebra.nonneg_TFAE View on Github →