Def InnerProductSpace.continuousLinearMapOfBilin

Modification history

2023-05-26 23:07

Mathlib/Analysis/InnerProductSpace/Dual.lean

feat: port Analysis.InnerProductSpace.Dual (#4402)

Added InnerProductSpace.continuousLinearMapOfBilin View on Github →