Theorem CStarAlgebra.nnnorm_mem_spectrum_of_nonneg

Modification history

2026-08-15 19:39

Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean

refactor(Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order): clean up hypotheses (#42545)

Modified CStarAlgebra.nnnorm_mem_spectrum_of_nonneg View on Github →

2024-09-12 16:24

Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean

chore: namespace lemmas to `CStarAlgebra` instead of `CStarRing` (#16653) …

Added CStarAlgebra.nnnorm_mem_spectrum_of_nonneg View on Github →