Mathlib Changelog
v4
Changelog
About
Github
Theorem
CStarAlgebra.nonneg_iff_exists_nonneg_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_nonneg_and_eq_mul_self
View on Github →