basic): the left-regular representation is an isometry for (even non-unital) C⋆-algebras (#16964)

Commit

3 years ago

feat(analysis/normed_space/basic): the left-regular representation is an isometry for (even non-unital) C⋆-algebras (#16964) This is a key tool to show that the multiplier algebra is a C⋆-algebra. - [x] depends on: #16963

Author

j-loreaux

Parents

1499a80b

mathlib3 b75fd415 - feat(analysis/normed_space/basic): the left-regular representation is an isometry for (even non-unital) C⋆-algebras (#16964)

mathlib3
b75fd415 - feat(analysis/normed_space/basic): the left-regular representation is an isometry for (even non-unital) C⋆-algebras (#16964)