Commit 2024-12-10 16:45 02c57768

View on Github →

feat(Analysis/Distribution): generalize linearity of SchwartzMap.bilinLeftCLM (#19823) Generalize SchwartzMap.bilinLeftCLM from ℝ-linearity to 𝕜-linearity with [NontriviallyNormedField 𝕜]. Add ContinuousLinearMap.bilinRestrictScalars for convenience.

Estimated changes

Modified Mathlib/Analysis/Distribution/SchwartzSpace.lean

modified def SchwartzMap.bilinLeftCLM

Modified Mathlib/Analysis/NormedSpace/OperatorNorm/Bilinear.lean

added def ContinuousLinearMap.bilinearRestrictScalars

added theorem ContinuousLinearMap.bilinearRestrictScalars_apply_apply

added theorem ContinuousLinearMap.bilinearRestrictScalars_eq_restrictScalarsL_comp_restrictScalars

added theorem ContinuousLinearMap.bilinearRestrictScalars_eq_restrictScalars_restrictScalarsL_comp

added theorem ContinuousLinearMap.norm_bilinearRestrictScalars