Commit 2024-08-01 03:42 a8a6183c

feat(CstarAlgebra): define Hilbert C⋆-modules (#15244) This PR defines Hilbert C⋆-modules. A Hilbert C⋆-module is a complex module E together with a right A-module structure, where A is a C⋆-algebra, and with an "inner product" that takes values in A. This inner product satisfies the Cauchy-Schwarz inequality, and induces a norm that makes E a normed vector space. This is a stepping stone towards proving that matrices with entries in a C⋆-algebra are a C⋆-algebra, which is in turn needed to define completely positive maps.