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