Theorem CStarAlgebra.pow_nonneg

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.pow_nonnegView on Github →