mathlib documentation

analysis.normed_space.star.mul

The left-regular representation is an isometry for Cā‹†-algebras #

@[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.

theorem mul_flip_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 right regular anti-representation is an isometry.