Theorem CStarRing.norm_le_one_iff_of_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.norm_le_one_iff_of_nonneg View on Github →

2024-08-31 15:30

Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean

feat: in a unital C⋆-algebra, `‖a‖ ≤ r ↔ a ≤ r • 1`, and related lemmas (#16266)

Added CStarRing.norm_le_one_iff_of_nonneg View on Github →