Theorem ContinuousLinearMap.precompL_apply

Modification history

2026-09-29 15:02
Mathlib/Analysis/Normed/Operator/Bilinear.lean
feat: introduce an IsNormableSpace class (#42983) …
Modified ContinuousLinearMap.precompL_applyView on Github →
2024-04-05 06:15
Mathlib/Analysis/NormedSpace/OperatorNorm/Bilinear.lean
feat: `deriv` versions of composition lemmas with bilinear maps (#11868) …
Added ContinuousLinearMap.precompL_applyView on Github →