Commit 2024-04-01 16:13 66c48ceb

View on Github →

feat: bundled versions of two operations on continuous multilinear maps (#11775) We provide versions of smulRight and compContinuousLinearMap as a continuous bilinear (resp multilinear) map.

Estimated changes

Modified Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean

added def ContinuousMultilinearMap.compContinuousLinearMapLRight

added theorem ContinuousMultilinearMap.compContinuousLinearMapLRight_apply

added theorem ContinuousMultilinearMap.norm_compContinuousLinearMapLRight_le

added def ContinuousMultilinearMap.smulRightL

added theorem ContinuousMultilinearMap.smulRightL_apply

Modified Mathlib/Topology/Algebra/Module/StrongTopology.lean

added theorem ContinuousLinearMap.toLinearMap₂_apply

Modified scripts/style-exceptions.txt