Def NormedSpace.Dual

Modification history

2023-09-11 20:08

Mathlib/Analysis/NormedSpace/Dual.lean

feat (NormedSpace.Dual): make `Dual` reducible (#6998) …

Deleted NormedSpace.Dual View on Github →

2023-05-25 08:46

Mathlib/Analysis/NormedSpace/Dual.lean

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

Added NormedSpace.Dual View on Github →