Theorem ContinuousLinearMap.bilinearRestrictScalars_apply_apply

Modification history

2024-12-10 16:45
Mathlib/Analysis/NormedSpace/OperatorNorm/Bilinear.lean
feat(Analysis/Distribution): generalize linearity of SchwartzMap.bilinLeftCLM (#19823) …
Added ContinuousLinearMap.bilinearRestrictScalars_apply_applyView on Github →