Mathlib Changelog
v4
Changelog
About
Github
Theorem
CStarAlgebra.conjugate_le_norm_smul'
Modification history
2024-09-12 16:24
Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean
chore: namespace lemmas to `CStarAlgebra` instead of `CStarRing` (#16653) …
Added
CStarAlgebra.conjugate_le_norm_smul'
View on Github →