Commit 2020-06-14 12:37 a6534db8

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.