Theorem ContinuousLinearMap.bilinearComp_zero

Modification history

2026-09-29 15:02
Mathlib/Analysis/Normed/Operator/Bilinear.lean
feat: introduce an IsNormableSpace class (#42983) …
Modified ContinuousLinearMap.bilinearComp_zeroView on Github →
2025-07-16 10:43
Mathlib/Analysis/NormedSpace/OperatorNorm/Bilinear.lean
feat: ContinuousLinearMap.flip/bilinearComp of zero (#27193) …
Added ContinuousLinearMap.bilinearComp_zeroView on Github →