Theorem IsBoundedBilinearMap.symm

Modification history

2025-05-15 20:48
Mathlib/Analysis/Normed/Operator/BoundedLinearMaps.lean
feat(MeasureTheory): characteristic function in a Banach space (#24836) …
Added IsBoundedBilinearMap.symmView on Github →