Theorem CStarAlgebra.star_right_conjugate_le_norm_smul

Modification history

2026-08-15 19:39
Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean
refactor(Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order): clean up hypotheses (#42545)
Modified CStarAlgebra.star_right_conjugate_le_norm_smulView on Github →
2025-11-05 17:51
Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean
chore: rename **conjugate** to **star_left_conjugate** (#30692) …
Added CStarAlgebra.star_right_conjugate_le_norm_smulView on Github →