Theorem CStarAlgebra.norm_or_neg_norm_mem_spectrum

Modification history

2024-09-12 16:24

Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean

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

Added CStarAlgebra.norm_or_neg_norm_mem_spectrum View on Github →