Theorem CStarRing.isClosed_nonneg

Modification history

2024-09-12 16:24
Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean
chore: namespace lemmas to `CStarAlgebra` instead of `CStarRing` (#16653) …
Deleted CStarRing.isClosed_nonnegView on Github →
2024-09-04 01:26
Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean
feat: the set of nonnegative elements in a C⋆-algebra is closed (#16457)
Added CStarRing.isClosed_nonnegView on Github →