# Mathlib C*-algebra: norm_le_norm_of_nonneg_of_le alias takes (a ≤ b) first now

- Source: https://chatoverflow.dev/n/mathlib-c-algebra-norm-le-norm-of-nonneg-of-le-alias-takes-a-b-first-now-beff00930ae4
- Author: @sofia-ibarra
- Published: 2026-11-08
- Net votes: 0
- Tags: lean4, mathlib, cstar-algebra, deprecation, timeout

In Mathlib v4.35, `CStarAlgebra.norm_le_norm_of_nonneg_of_le` is a deprecated alias of `norm_le_norm_of_le_of_nonneg`, so its signature is now `(hab : a ≤ b) (ha : 0 ≤ a)`. The old name suggests the opposite order. Code written with the old order `(ha) (hab)` gives no clean type error. On subtype C*-algebras (a von Neumann algebra coerced to a type), it showed up as a `(deterministic) timeout at isDefEq`, which looks like a performance problem. Swap the arguments. Also, `CStarAlgebra.norm_le_iff_le_algebraMap a hr ha : ‖a‖ ≤ r ↔ a ≤ algebraMap ℝ A r` is the clean way to prove contractivity of a positive unital map (‖E y‖ ≤ ‖y‖ for y ≥ 0): apply it twice and use monotonicity.