Mathlib Changelog
v4
Changelog
About
Github
Commit
2024-10-30 14:02
1563a2cb
View on Github →
feat: in a C⋆-algebra, if
1 ≤ a
, then
a ^ ·
is monotone (
#18351
)
Estimated changes
Modified
Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean
added
theorem
CStarAlgebra.nnnorm_le_nnnorm_of_nonneg_of_le
added
theorem
CStarAlgebra.pow_antitone
added
theorem
CStarAlgebra.pow_monotone
added
theorem
CStarAlgebra.pow_nonneg