Theorem IsBoundedBilinearMap.symm

Modification history

2026-01-20 20:25
Mathlib/Analysis/Normed/Operator/BoundedLinearMaps.lean
feat(Analysis/Normed): generalize `smul` on cts [multi-]linear maps (#33962) …
Modified IsBoundedBilinearMap.symmView on Github →
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 →