# Commit 2020-06-14 12:37 a6534db8

View on Github →feat(normed_space/dual): (topological) dual of a normed space (#3021)
Define the topological dual of a normed space, and prove that over the reals, the inclusion into the double dual is an isometry.
Supporting material: a corollary of Hahn-Banach; material about spans of singletons added to `linear_algebra.basic`

and `normed_space.operator_norm`

; material about homotheties added to `normed_space.operator_norm`

.