Theorem CStarAlgebra.nnnorm_le_nnnorm_of_nonneg_of_le

Modification history

2024-10-30 14:02
Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean
feat: in a C⋆-algebra, if `1 ≤ a`, then `a ^ ·` is monotone (#18351)
Added CStarAlgebra.nnnorm_le_nnnorm_of_nonneg_of_leView on Github →