mathlib3 documentation

analysis.normed_space.star.mul

The left-regular representation is an isometry for C⋆-algebras #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

@[simp]
theorem op_nnnorm_mul (𝕜 : Type u_1) {E : Type u_2} [densely_normed_field 𝕜] [non_unital_normed_ring E] [star_ring E] [cstar_ring E] [normed_space 𝕜 E] [is_scalar_tower 𝕜 E E] [smul_comm_class 𝕜 E E] (a : E) :

In a C⋆-algebra E, either unital or non-unital, multiplication on the left by a : E has norm equal to the norm of a.

@[simp]
theorem op_nnnorm_mul_flip (𝕜 : Type u_1) {E : Type u_2} [densely_normed_field 𝕜] [non_unital_normed_ring E] [star_ring E] [cstar_ring E] [normed_space 𝕜 E] [is_scalar_tower 𝕜 E E] [smul_comm_class 𝕜 E E] (a : E) :

In a C⋆-algebra E, either unital or non-unital, multiplication on the right by a : E has norm eqaul to the norm of a.

theorem mul_isometry (𝕜 : Type u_1) (E : Type u_2) [densely_normed_field 𝕜] [non_unital_normed_ring E] [star_ring E] [cstar_ring E] [normed_space 𝕜 E] [is_scalar_tower 𝕜 E E] [smul_comm_class 𝕜 E E] :

In a C⋆-algebra E, either unital or non-unital, the left regular representation is an isometry.

In a C⋆-algebra E, either unital or non-unital, the right regular anti-representation is an isometry.