Theorem CStarAlgebra.nnnorm_le_nnnorm_of_le_of_nonneg

Modification history

2026-08-15 19:39
Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean
refactor(Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order): clean up hypotheses (#42545)
Added CStarAlgebra.nnnorm_le_nnnorm_of_le_of_nonnegView on Github →