Theorem CStarRing.star_mul_le_algebraMap_norm_sq

Modification history

2024-09-12 16:24

Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean

chore: namespace lemmas to `CStarAlgebra` instead of `CStarRing` (#16653) …

Deleted CStarRing.star_mul_le_algebraMap_norm_sq View on Github →

2024-08-06 04:16

Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean

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

Added CStarRing.star_mul_le_algebraMap_norm_sq View on Github →