Theorem CStarRing.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) …

Deleted CStarRing.conjugate_le_norm_smul'View on Github →

2024-08-31 15:30

Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean

feat: in a unital C⋆-algebra, `‖a‖ ≤ r ↔ a ≤ r • 1`, and related lemmas (#16266)

Modified CStarRing.conjugate_le_norm_smul'View on Github →

2024-08-06 04:16

Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean

chore(*): rename `Cstar*` to `CStar*` (#15495) …

Added CStarRing.conjugate_le_norm_smul'View on Github →