Theorem CStarAlgebra.nonneg_iff_exists_isSelfAdjoint_and_eq_mul_self

Modification history

2025-09-27 15:46
Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Basic.lean
chore(Analysis/SpecialFunctions/CFC/Rpow/Basic): fix confusing names (#30031) …
Added CStarAlgebra.nonneg_iff_exists_isSelfAdjoint_and_eq_mul_selfView on Github →