Def InnerProductSpace.toDualMap

Modification history

2023-05-26 23:07

Mathlib/Analysis/InnerProductSpace/Dual.lean

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

Added InnerProductSpace.toDualMap View on Github →