Commit 2025-07-16 10:43 5726d730

View on Github →

feat: ContinuousLinearMap.flip/bilinearComp of zero (#27193) From the Brownian motion project.

Estimated changes

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

added theorem ContinuousLinearMap.bilinearComp_zero

added theorem ContinuousLinearMap.bilinearComp_zero_left

added theorem ContinuousLinearMap.bilinearComp_zero_right

added theorem ContinuousLinearMap.flip_zero