Def InnerProductSpace.toDual

Modification history

2023-05-26 23:07

Mathlib/Analysis/InnerProductSpace/Dual.lean

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

Added InnerProductSpace.toDual View on Github →