Commit 2022-06-01 09:18 2a0f4743
View on Github →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.