Documentation

Mathlib.Analysis.Normed.Algebra.Basic

Normed algebras #

This file contains basic facts about normed algebras.

Main results #

TODO #

Tags #

normed algebra, character space, continuous functional calculus

theorem WeakDual.CharacterSpace.norm_le_norm_one {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] [CompleteSpace A] (φ : (WeakDual.characterSpace 𝕜 A)) :
WeakDual.toNormedDual φ 1