mathlib

2a0f4743 - feat(analysis/normed_space/star/character_space): compactness of the character space of a normed algebra (#14135)

feat(analysis/normed_space/star/character_space): compactness of the character space of a normed algebra (#14135) This PR puts a `compact_space` instance on `character_space 𝕜 A` for a normed algebra `A` using the Banach-Alaoglu theorem. This is a key step in developing the continuous functional calculus. Co-authored-by: Frédéric Dupuis <31101893+dupuisf@users.noreply.github.com>