Theorem isBoundedBilinearMap_inner

Modification history

2024-09-25 20:50
Mathlib/Analysis/InnerProductSpace/Basic.lean
chore(Analysis/InnerProductSpace): weaken assumptions to `SeminormedAddCommGroup` (#17007) …
Modified isBoundedBilinearMap_innerView on Github →
2023-05-25 17:58
Mathlib/Analysis/InnerProductSpace/Basic.lean
feat: port Analysis.InnerProductSpace.Basic (#4280) …
Added isBoundedBilinearMap_innerView on Github →