Def NormedSpace.inclusionInDoubleDual

Modification history

2023-05-25 08:46

Mathlib/Analysis/NormedSpace/Dual.lean

feat: port Analysis.NormedSpace.Dual (#4310)

Added NormedSpace.inclusionInDoubleDual View on Github →