mathlib3

e31f0319 - feat(analysis/locally_convex): polar sets for dualities (#12849)

feat(analysis/locally_convex): polar sets for dualities (#12849) Define the absolute polar for a duality and prove easy properties such as * `linear_map.polar_eq_Inter`: The polar as an intersection. * `linear_map.subset_bipolar`: The polar is a subset of the bipolar. * `linear_map.polar_weak_closed`: The polar is closed in the weak topology induced by `B.flip`. Moreover, the corresponding lemmas are removed in the normed space setting as they all follow directly from the general case.