Mathlib Changelog
v4
Changelog
About
Github
Commit
2024-09-04 01:26
8056127e
View on Github ā
feat: the set of nonnegative elements in a Cā-algebra is closed (
#16457
)
Estimated changes
Modified
Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean
added
theorem
CStarRing.isClosed_nonneg