Structures · Analysis

RegularNormedAlgebra

This is a mixin class for non-unital normed algebras which states that the left-regular representation of the algebra on itself is isometric. Every unital normed algebra with ‖1‖ = 1 is a regular normed algebra (see NormedAlgebra.instRegularNormedAlgebra). In addition, so is every C⋆-algebra, non-unital included (see CStarRing.instRegularNormedAlgebra), but there are yet other examples. Any algebra with an approximate identity (e.g., L¹) is also regular. This is a useful class because it gives rise to a nice norm on the unitization; in particular it is a C⋆-norm when the norm on A is a C⋆-norm.

Defined in

Mathlib.Analysis.Normed.Operator.Mul

Shape

2 explicit arguments · adds isometry_mul'