# Commit 2024-08-01 03:42 a8a6183c

View on Github →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.