mathlib3

91c0ef86 - feat(analysis/normed_space/weak_dual): add the rest of Banach-Alaoglu theorem (#9862)

feat(analysis/normed_space/weak_dual): add the rest of Banach-Alaoglu theorem (#9862) The second of two parts to add the Banach-Alaoglu theorem about the compactness of the closed unit ball (and more generally polar sets of neighborhoods of the origin) of the dual of a normed space in the weak-star topology. This second half is about the embedding of the weak dual of a normed space into a (big) product of the ground fields, and the required compactness statements from Tychonoff's theorem. In particular it contains the actual Banach-Alaoglu theorem. Co-Authored-By: Yury Kudryashov <urkud@urkud.name> Co-authored-by: kkytola <39528102+kkytola@users.noreply.github.com>