Normed algebras #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file contains basic facts about normed algebras.
Main results #
- We show that the character space of a normed algebra is compact using the Banach-Alaoglu theorem.
TODO #
- Show compactness for topological vector spaces; this requires the TVS version of Banach-Alaoglu.
Tags #
normed algebra, character space, continuous functional calculus
theorem
weak_dual.character_space.norm_le_norm_one
{𝕜 : Type u_1}
{A : Type u_2}
[nontrivially_normed_field 𝕜]
[normed_ring A]
[normed_algebra 𝕜 A]
[complete_space A]
(φ : ↥(weak_dual.character_space 𝕜 A)) :
@[protected, instance]
def
weak_dual.character_space.compact_space
{𝕜 : Type u_1}
{A : Type u_2}
[nontrivially_normed_field 𝕜]
[normed_ring A]
[normed_algebra 𝕜 A]
[complete_space A]
[proper_space 𝕜] :