Commit 2021-04-21 19:58 253d4f5b

feat(analysis/normed_space/dual): generalize to seminormed space (#7262) We generalize here the Hahn-Banach theorem and the notion of dual space to semi_normed_space.