Theorem ContinuousLinearMap.opNorm_lsmul_apply

Modification history

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