Theorem CStarAlgebra.nonneg_iff_eq_nonneg_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) …
Deleted CStarAlgebra.nonneg_iff_eq_nonneg_mul_selfView 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_iff_eq_nonneg_mul_selfView on Github →