Commit 2025-11-17 16:20 fe1548c3

View on Github →

chore(Normed/Operator): add smulRightL_apply_apply (#31642)

Estimated changes

Modified Mathlib/Analysis/Calculus/ParametricIntegral.lean

Modified Mathlib/Analysis/Normed/Operator/Bilinear.lean

modified theorem ContinuousLinearMap.norm_smulRightL_apply