Theorem CStarAlgebra.pow_antitone

Modification history

2026-08-15 19:39
Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean
refactor(Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order): clean up hypotheses (#42545)
Modified CStarAlgebra.pow_antitoneView on Github →
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_antitoneView on Github →