Theorem CStarAlgebra.nonneg_iff_eq_sqrt_mul_sqrt

Modification history

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_sqrt_mul_sqrtView on Github →