Theorem ContinuousLinearMap.opNNNorm_lsmul_le

Modification history

2026-06-01 19:58
Mathlib/Analysis/Normed/Operator/Mul.lean
feat: more basic lemmas on norms and sums (#40100)
Added ContinuousLinearMap.opNNNorm_lsmul_leView on Github →