Theorem CStarAlgebra.conjugate_le_norm_smul'

Modification history

2025-11-05 17:51

Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean

chore: rename **conjugate** to **star_left_conjugate** (#30692) …

Deleted CStarAlgebra.conjugate_le_norm_smul'View on Github →

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 →