Commit 2024-09-23 11:56 ac537a4a

chore: generalize IsBoundedBilinearMap to seminormed spaces (#17011) The claim in Mathlib/Analysis/NormedSpace/OperatorNorm/NormedSpace.lean that

This file contains statements about operator norm for which it really matters that the underlying space has a norm (rather than just a seminorm). was not entirely true. The main trick is to case on whether the norm of an element is zero, rather than on that element itself being zero. Unfortunately this causes some minor elaboration issues downstream, but they are easy to work around.